let j be Nat; :: thesis: for D being non empty set
for p being Element of D
for f being FinSequence of D st p in rng f & j + 1 in dom (f :- p) holds
(f :- p) /. (j + 1) = f /. (j + (p .. f))
let D be non empty set ; :: thesis: for p being Element of D
for f being FinSequence of D st p in rng f & j + 1 in dom (f :- p) holds
(f :- p) /. (j + 1) = f /. (j + (p .. f))
let p be Element of D; :: thesis: for f being FinSequence of D st p in rng f & j + 1 in dom (f :- p) holds
(f :- p) /. (j + 1) = f /. (j + (p .. f))
let f be FinSequence of D; :: thesis: ( p in rng f & j + 1 in dom (f :- p) implies (f :- p) /. (j + 1) = f /. (j + (p .. f)) )
assume that
A1: p in rng f and
A2: j + 1 in dom (f :- p) ; :: thesis: (f :- p) /. (j + 1) = f /. (j + (p .. f))
A3: j + (p .. f) in dom f by A1, A2, Th51;
set i = j + 1;
A4: p .. f <= len f by A1, FINSEQ_4:21;
consider k being Element of NAT such that
A5: k + 1 = p .. f and
A6: f :- p = f /^ k by A1, Th49;
k <= p .. f by A5, NAT_1:11;
then A7: k <= len f by A4, XXREAL_0:2;
thus (f :- p) /. (j + 1) = (f :- p) . (j + 1) by A2, PARTFUN1:def 6
.= f . ((j + 1) + k) by A2, A6, A7, RFINSEQ:def 1
.= f /. (j + (p .. f)) by A5, A3, PARTFUN1:def 6 ; :: thesis: verum