let IT be FinSequence; ( ( 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; ( 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
; ( 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 ( (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)
;
( (len IT) + 1 = len fs & ( for b being Nat holds
( ( b < a implies IT . b = fs . b ) & ( b >= a implies IT . b2 = fs . (b2 + 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
;
for b being Nat holds
( ( b < a implies IT . b = fs . b ) & ( b >= a implies IT . b2 = fs . (b2 + 1) ) )let b be
Nat;
( ( b < a implies IT . b = fs . b ) & ( b >= a implies IT . b1 = fs . (b1 + 1) ) )thus
(
b < a implies
IT . b = fs . b )
by A2, FINSEQ_3:110;
( b >= a implies IT . b1 = fs . (b1 + 1) )assume A4:
b >= a
;
IT . b1 = fs . (b1 + 1)
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) ) )
; IT = Del (fs,a)
A9:
for k being Nat st 1 <= k & k <= len IT holds
IT . k = (Del (fs,a)) . k
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; verum