let IT be FinSequence; :: thesis: ( ( not a in dom fs implies ( IT = Del fs,a iff IT = fs ) ) & ( a in dom fs implies ( IT = Del fs,a iff ( (len IT) + 1 = len fs & ( for b being Nat holds
( ( b < a implies IT . b = fs . b ) & ( b >= a implies IT . b = fs . (b + 1) ) ) ) ) ) ) )
thus ( not a in dom fs implies ( IT = Del fs,a iff IT = fs ) ) by FINSEQ_3:113; :: thesis: ( a in dom fs implies ( IT = Del fs,a iff ( (len IT) + 1 = len fs & ( for b being Nat holds
( ( b < a implies IT . b = fs . b ) & ( b >= a implies IT . b = fs . (b + 1) ) ) ) ) ) )
assume A1: a in dom fs ; :: thesis: ( IT = Del fs,a iff ( (len IT) + 1 = len fs & ( for b being Nat holds
( ( b < a implies IT . b = fs . b ) & ( b >= a implies IT . b = fs . (b + 1) ) ) ) ) )
A2: a in NAT by ORDINAL1:def 13;

hereby :: thesis: ( (len IT) + 1 = len fs & ( for b being Nat holds
( ( b < a implies IT . b = fs . b ) & ( b >= a implies IT . b = fs . (b + 1) ) ) ) implies IT = Del fs,a )

assume A3: IT = Del fs,a ; :: thesis: ( (len IT) + 1 = len fs & ( for b being Nat holds
( ( b < a implies IT . b = fs . b ) & ( b >= a implies IT . b₂ = fs . (b₂ + 1) ) ) ) )
then consider m being Nat such that
A4: ( len fs = m + 1 & len IT = m ) by A1, FINSEQ_3:113;
thus (len IT) + 1 = len fs by A4; :: thesis: for b being Nat holds
( ( b < a implies IT . b = fs . b ) & ( b >= a implies IT . b₂ = fs . (b₂ + 1) ) )
let b be Nat; :: thesis: ( ( b < a implies IT . b = fs . b ) & ( b >= a implies IT . b₁ = fs . (b₁ + 1) ) )
X: b in NAT by ORDINAL1:def 13;
hence ( b < a implies IT . b = fs . b ) by A2, A3, A4, FINSEQ_3:119; :: thesis: ( b >= a implies IT . b₁ = fs . (b₁ + 1) )
assume A5: b >= a ; :: thesis: IT . b₁ = fs . (b₁ + 1)

per cases ( b <= len IT or b > len IT ) ;

suppose b <= len IT ; :: thesis: IT . b₁ = fs . (b₁ + 1)

hence IT . b = fs . (b + 1) by A1, A3, A4, A5, X, FINSEQ_3:120; :: thesis: verum

end;

suppose A6: b > len IT ; :: thesis: IT . b₁ = fs . (b₁ + 1)

then not b in dom IT by FINSEQ_3:27;
then A7: IT . b = {} by FUNCT_1:def 4;
b + 1 > (len IT) + 1 by A6, XREAL_1:8;
then not b + 1 in dom fs by A4, FINSEQ_3:27;
hence IT . b = fs . (b + 1) by A7, FUNCT_1:def 4; :: thesis: verum

end;

end;

end;

assume A8: ( (len IT) + 1 = len fs & ( for b being Nat holds
( ( b < a implies IT . b = fs . b ) & ( b >= a implies IT . b = fs . (b + 1) ) ) ) ) ; :: thesis: IT = Del fs,a
consider m being Nat such that
A9: ( len fs = m + 1 & len (Del fs,a) = m ) by A1, FINSEQ_3:113;
for k being Nat st 1 <= k & k <= len IT holds
IT . k = (Del fs,a) . k

proof

let k be Nat; :: thesis: ( 1 <= k & k <= len IT implies IT . k = (Del fs,a) . k )
assume A10: ( 1 <= k & k <= len IT ) ; :: thesis: IT . k = (Del fs,a) . k
reconsider k = k as Element of NAT by ORDINAL1:def 13;

per cases ( k < a or k >= a ) ;

suppose A11: k < a ; :: thesis: IT . k = (Del fs,a) . k

then IT . k = fs . k by A8;
hence IT . k = (Del fs,a) . k by A2, A8, A11, FINSEQ_3:119; :: thesis: verum

end;

suppose A12: k >= a ; :: thesis: IT . k = (Del fs,a) . k

then IT . k = fs . (k + 1) by A8;
hence IT . k = (Del fs,a) . k by A1, A8, A10, A12, FINSEQ_3:120; :: thesis: verum

end;

end;

end;

hence IT = Del fs,a by A8, A9, FINSEQ_1:18; :: thesis: verum