let k, n be Nat; :: thesis: for f being FinSequence st k < n holds
(Del (f,n)) . k = f . k
let f be FinSequence; :: thesis: ( k < n implies (Del (f,n)) . k = f . k )
assume A1: k < n ; :: thesis: (Del (f,n)) . k = f . k
per cases ( ( n in dom f & f <> {} ) or not n in dom f or f = {} ) ;
suppose that A2: n in dom f and
A3: f <> {} ; :: thesis: (Del (f,n)) . k = f . k
consider m being Nat such that
A4: len f = m + 1 by A3, NAT_1:6;
now :: thesis: (Del (f,n)) . k = f . k
per cases ( 1 <= k or not 1 <= k ) ;
suppose A5: 1 <= k ; :: thesis: (Del (f,n)) . k = f . k
set X = (dom f) \ {n};
A6: dom (Sgm ((dom f) \ {n})) = Seg (len (Sgm ((dom f) \ {n}))) by FINSEQ_1:def 3;
A7: dom f = Seg (len f) by FINSEQ_1:def 3;
then A8: len (Sgm ((dom f) \ {n})) = m by A4, A2, Th105;
(dom f) \ {n} c= Seg (len f) by A7, XBOOLE_1:36;
then rng (Sgm ((dom f) \ {n})) = (dom f) \ {n} by FINSEQ_1:def 13;
then A9: dom (f * (Sgm ((dom f) \ {n}))) = dom (Sgm ((dom f) \ {n})) by RELAT_1:27, XBOOLE_1:36;
n <= m + 1 by A4, A2, Th25;
then k < m + 1 by A1, XXREAL_0:2;
then k <= m by NAT_1:13;
then A10: k in Seg m by A5, FINSEQ_1:1;
then ( 1 <= k & k < n implies (Sgm ((dom f) \ {n})) . k = k ) by A4, A2, A7, Th106;
hence (Del (f,n)) . k = f . k by A1, A5, A10, A6, A9, A8, FUNCT_1:12; :: thesis: verum
end;
suppose A11: not 1 <= k ; :: thesis: (Del (f,n)) . k = f . k
Seg (len (Del (f,n))) = Seg m by A4, A2, Th107;
then dom (Del (f,n)) = Seg m by FINSEQ_1:def 3;
then A12: not k in dom (Del (f,n)) by A11, FINSEQ_1:1;
not k in dom f by A11, Th25;
then f . k = {} by FUNCT_1:def 2;
hence (Del (f,n)) . k = f . k by A12, FUNCT_1:def 2; :: thesis: verum
end;
end;
end;
hence (Del (f,n)) . k = f . k ; :: thesis: verum
end;
suppose ( not n in dom f or f = {} ) ; :: thesis: (Del (f,n)) . k = f . k
hence (Del (f,n)) . k = f . k by Th102; :: thesis: verum
end;
end;