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))
set i = j + 1;
consider k being Element of NAT such that
A3: k + 1 = p .. f and
A4: f :- p = f /^ k by A1, Th52;
( k <= p .. f & p .. f <= len f ) by A1, A3, FINSEQ_4:31, NAT_1:11;
then A5: k <= len f by XXREAL_0:2;
A6: j + (p .. f) in dom f by A1, A2, Th54;
thus (f :- p) /. (j + 1) = (f :- p) . (j + 1) by A2, PARTFUN1:def 8
.= f . ((j + 1) + k) by A2, A4, A5, RFINSEQ:def 2
.= f /. (j + (p .. f)) by A3, A6, PARTFUN1:def 8 ; :: thesis: verum