let f be FinSequence; :: thesis: for n, m, k being Nat st len f = m + 1 & n in dom f & k in Seg m & not (Del (f,n)) . k = f . k holds
(Del (f,n)) . k = f . (k + 1)
let n, m, k be Nat; :: thesis: ( len f = m + 1 & n in dom f & k in Seg m & not (Del (f,n)) . k = f . k implies (Del (f,n)) . k = f . (k + 1) )
assume that
A1: ( len f = m + 1 & n in dom f ) and
A2: k in Seg m ; :: thesis: ( (Del (f,n)) . k = f . k or (Del (f,n)) . k = f . (k + 1) )
set X = (dom f) \ {n};
A3: dom f = Seg (len f) by FINSEQ_1:def 3;
then A4: ( n <= k & k <= m implies (Sgm ((dom f) \ {n})) . k = k + 1 ) by A1, A2, FINSEQ_3:108;
rng (Sgm ((dom f) \ {n})) = (dom f) \ {n} by FINSEQ_1:def 14;
then A5: dom (f * (Sgm ((dom f) \ {n}))) = dom (Sgm ((dom f) \ {n})) by RELAT_1:27, XBOOLE_1:36;
A6: ( dom (Sgm ((dom f) \ {n})) = Seg (len (Sgm ((dom f) \ {n}))) & Del (f,n) = f * (Sgm ((dom f) \ {n})) ) by FINSEQ_1:def 3, FINSEQ_3:def 2;
A7: len (Sgm ((dom f) \ {n})) = m by A1, A3, FINSEQ_3:107;
( 1 <= k & k < n implies (Sgm ((dom f) \ {n})) . k = k ) by A1, A2, A3, FINSEQ_3:108;
hence ( (Del (f,n)) . k = f . k or (Del (f,n)) . k = f . (k + 1) ) by A2, A6, A5, A7, A4, FINSEQ_3:25, FUNCT_1:12; :: thesis: verum