let f be FinSequence; :: thesis: for n, m, k being Element of NAT st len f = m + 1 & k < n holds
(Del f,n) . k = f . k
let n, m, k be Element of NAT ; :: thesis: ( len f = m + 1 & k < n implies (Del f,n) . k = f . k )
assume A1: ( len f = m + 1 & k < n ) ; :: thesis: (Del f,n) . k = f . k

per cases ( n in dom f or not n in dom f ) ;

suppose A2: n in dom f ; :: thesis: (Del f,n) . k = f . k

now

per cases ( 1 <= k or not 1 <= k ) ;

suppose A3: 1 <= k ; :: thesis: (Del f,n) . k = f . k

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

end;

suppose A8: not 1 <= k ; :: thesis: (Del f,n) . k = f . k

then not k in dom f by Th27;
then A9: f . k = {} by FUNCT_1:def 4;
Seg (len (Del f,n)) = Seg m by A1, A2, Th118;
then dom (Del f,n) = Seg m by FINSEQ_1:def 3;
then not k in dom (Del f,n) by A8, FINSEQ_1:3;
hence (Del f,n) . k = f . k by A9, FUNCT_1:def 4; :: thesis: verum

end;

end;

end;

hence (Del f,n) . k = f . k ; :: thesis: verum

end;

suppose not n in dom f ; :: thesis: (Del f,n) . k = f . k

hence (Del f,n) . k = f . k by Th113; :: thesis: verum

end;

end;