let f be FinSequence; :: thesis: for n, m, k being Element of 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 Element of 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 A1: ( len f = m + 1 & n in dom f & k in Seg m ) ; :: thesis: ( (Del f,n) . k = f . k or (Del f,n) . k = f . (k + 1) )
set X = (dom f) \ {n};
A2: ( dom f = Seg (len f) & dom (Sgm ((dom f) \ {n})) = Seg (len (Sgm ((dom f) \ {n}))) ) by FINSEQ_1:def 3;
then A3: ( Del f,n = f * (Sgm ((dom f) \ {n})) & (dom f) \ {n} c= Seg (len f) ) by FINSEQ_3:def 2, XBOOLE_1:36;
then rng (Sgm ((dom f) \ {n})) = (dom f) \ {n} by FINSEQ_1:def 13;
then A4: ( dom (f * (Sgm ((dom f) \ {n}))) = dom (Sgm ((dom f) \ {n})) & len (Sgm ((dom f) \ {n})) = m ) by A1, A2, A3, FINSEQ_3:116, RELAT_1:46;
( ( 1 <= k & k < n implies (Sgm ((dom f) \ {n})) . k = k ) & ( n <= k & k <= m implies (Sgm ((dom f) \ {n})) . k = k + 1 ) ) by A1, A2, FINSEQ_3:117;
hence ( (Del f,n) . k = f . k or (Del f,n) . k = f . (k + 1) ) by A1, A2, A3, A4, FINSEQ_3:27, FUNCT_1:22; :: thesis: verum