let D be non empty set ; :: thesis: for p being Element of D
for f being FinSequence of D st p in rng f holds
(f :- p) /. (len (f :- p)) = f /. (len f)
let p be Element of D; :: thesis: for f being FinSequence of D st p in rng f holds
(f :- p) /. (len (f :- p)) = f /. (len f)
let f be FinSequence of D; :: thesis: ( p in rng f implies (f :- p) /. (len (f :- p)) = f /. (len f) )
A1: len (f :- p) in dom (f :- p) by Th6;
assume A2: p in rng f ; :: thesis: (f :- p) /. (len (f :- p)) = f /. (len f)
then p .. f <= len f by FINSEQ_4:21;
then reconsider j = (len f) - (p .. f) as Element of NAT by INT_1:5;
len (f :- p) = j + 1 by A2, Th50;
hence (f :- p) /. (len (f :- p)) = f /. (j + (p .. f)) by A2, A1, Th52
.= f /. (len f) ;
:: thesis: verum