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 . 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 ; :: thesis: for b being Nat holds
( ( b < a implies IT . b = fs . b ) & ( b >= a implies IT . b2 = fs . (b2 + 1) ) )
let b be Nat; :: thesis: ( ( 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; :: thesis: ( b >= a implies IT . b1 = fs . (b1 + 1) )
assume A4: b >= a ; :: thesis: IT . b1 = fs . (b1 + 1)
per cases ( b <= len IT or b > len IT ) ;
suppose b <= len IT ; :: thesis: IT . b1 = fs . (b1 + 1)
hence IT . b = fs . (b + 1) by A1, A2, A3, A4, FINSEQ_3:111; :: 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