let k, m, n be Nat; for f being FinSequence st len f = m + 1 & n in dom f & n <= k & k <= m holds
(Del (f,n)) . k = f . (k + 1)
let f be FinSequence; ( len f = m + 1 & n in dom f & n <= k & k <= m implies (Del (f,n)) . k = f . (k + 1) )
assume that
A1:
len f = m + 1
and
A2:
n in dom f
and
A3:
n <= k
and
A4:
k <= m
; (Del (f,n)) . k = f . (k + 1)
set X = (dom f) \ {n};
A5:
dom f = Seg (len f)
by FINSEQ_1:def 3;
then
(dom f) \ {n} c= Seg (len f)
by XBOOLE_1:36;
then
rng (Sgm ((dom f) \ {n})) = (dom f) \ {n}
by FINSEQ_1:def 13;
then A6:
dom (f * (Sgm ((dom f) \ {n}))) = dom (Sgm ((dom f) \ {n}))
by RELAT_1:27, XBOOLE_1:36;
A7:
len (Sgm ((dom f) \ {n})) = m
by A1, A2, A5, Th105;
A8:
dom (Sgm ((dom f) \ {n})) = Seg (len (Sgm ((dom f) \ {n})))
by FINSEQ_1:def 3;
1 <= n
by A2, Th25;
then
1 <= k
by A3, XXREAL_0:2;
then A9:
k in Seg m
by A4, FINSEQ_1:1;
then
( n <= k & k <= m implies (Sgm ((dom f) \ {n})) . k = k + 1 )
by A1, A2, A5, Th106;
hence
(Del (f,n)) . k = f . (k + 1)
by A3, A4, A9, A8, A6, A7, FUNCT_1:12; verum