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:104; :: 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 A2: 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 A3: ex m being Nat st
( len fs = m + 1 & len IT = m ) by A1, FINSEQ_3:104;
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 A2, FINSEQ_3:110; :: thesis: ( b >= a implies IT . b₁ = fs . (b₁ + 1) )
assume A4: 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, A2, A3, A4, FINSEQ_3:111; :: thesis: verum

end;

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

then not b in dom IT by FINSEQ_3:25;
then A6: IT . b = {} by FUNCT_1:def 2;
b + 1 > (len IT) + 1 by A5, XREAL_1:6;
then not b + 1 in dom fs by A3, FINSEQ_3:25;
hence IT . b = fs . (b + 1) by A6, FUNCT_1:def 2; :: thesis: verum

end;

end;

end;

assume that
A7: (len IT) + 1 = len fs and
A8: 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)
A9: 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
A10: k <= len IT ; :: thesis: IT . k = (Del (fs,a)) . k
reconsider k = k as Element of NAT by ORDINAL1:def 12;

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 A11, FINSEQ_3:110; :: 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, A7, A10, A12, FINSEQ_3:111; :: thesis: verum

end;

end;

end;

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