let f be FinSequence; :: thesis: for n, m, k being Element of NAT st len f = m + 1 & n in dom f & n <= k & k <= m 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 & n <= k & k <= m implies (Del f,n) . k = f . (k + 1) )
assume A1: ( len f = m + 1 & n in dom f & n <= k & k <= m ) ; :: thesis: (Del f,n) . k = f . (k + 1)
then 1 <= n by Th27;
then 1 <= k by A1, XXREAL_0:2;
then A2: k in Seg m by A1, FINSEQ_1:3;
set X = (dom f) \ {n};
A3: ( dom f = Seg (len f) & dom (Sgm ((dom f) \ {n})) = Seg (len (Sgm ((dom f) \ {n}))) ) by FINSEQ_1:def 3;
then A4: ( Del f,n = f * (Sgm ((dom f) \ {n})) & (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 A5: ( dom (f * (Sgm ((dom f) \ {n}))) = dom (Sgm ((dom f) \ {n})) & len (Sgm ((dom f) \ {n})) = m ) by A1, A3, A4, Th116, RELAT_1:46;
( n <= k & k <= m implies (Sgm ((dom f) \ {n})) . k = k + 1 ) by A1, A2, A3, Th117;
hence (Del f,n) . k = f . (k + 1) by A1, A2, A3, A5, FUNCT_1:22; :: thesis: verum