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) ) ) ) ) )

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 A4: ex m being Nat st
( len fs = m + 1 & len IT = m ) by A1, FINSEQ_3:113;
hence (len IT) + 1 = len fs ; :: 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) ) )
thus ( b < a implies IT . b = fs . b ) by A3, FINSEQ_3:119; :: thesis: ( b >= a implies IT . b₁ = fs . (b₁ + 1) )
assume A6: 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, A6, FINSEQ_3:120; :: thesis: verum

end;

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

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

end;

end;

end;

assume that
A9: (len IT) + 1 = len fs and
A10: 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)
A11: 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 that
1 <= k and
A12: 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 A13: k < a ; :: thesis: IT . k = (Del (fs,a)) . k

then IT . k = fs . k by A10;
hence IT . k = (Del (fs,a)) . k by A13, FINSEQ_3:119; :: thesis: verum

end;

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

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

end;

end;

end;

ex m being Nat st
( len fs = m + 1 & len (Del (fs,a)) = m ) by A1, FINSEQ_3:113;
hence IT = Del (fs,a) by A9, A11, FINSEQ_1:18; :: thesis: verum