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 that
A1: len f = m + 1 and
A2: k < n ; :: thesis: (Del f,n) . k = f . k

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

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

now

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

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

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

end;

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

Seg (len (Del f,n)) = Seg m by A1, A3, Th118;
then dom (Del f,n) = Seg m by FINSEQ_1:def 3;
then A11: not k in dom (Del f,n) by A10, FINSEQ_1:3;
not k in dom f by A10, Th27;
then f . k = {} by FUNCT_1:def 4;
hence (Del f,n) . k = f . k by A11, 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;