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