let n be Nat; :: thesis: for M being FinSequence st len M = n + 1 holds
M = (Del M,(len M)) ^ <*(M . (len M))*>
let M be FinSequence; :: thesis: ( len M = n + 1 implies M = (Del M,(len M)) ^ <*(M . (len M))*> )
assume A1: len M = n + 1 ; :: thesis: M = (Del M,(len M)) ^ <*(M . (len M))*>
then M <> {} ;
then consider q being FinSequence, x being set such that
A2: M = q ^ <*x*> by FINSEQ_1:63;
reconsider n = n as Element of NAT by ORDINAL1:def 13;
A3: n + 1 = n + 1 ;
A4: len M = (len q) + (len <*x*>) by A2, FINSEQ_1:35
.= (len q) + 1 by FINSEQ_1:56 ;
then A5: M . (len M) = x by A2, FINSEQ_1:59;
A6: len (Del M,(len M)) = len q by A4, Th3;
X: dom q = Seg (len q) by FINSEQ_1:def 3;

now

let i be Nat; :: thesis: ( i in dom q implies (Del M,(len M)) . i = q . i )
assume A7: i in dom q ; :: thesis: (Del M,(len M)) . i = q . i
then A8: i in dom q ;
A9: i in NAT by ORDINAL1:def 13;
( 1 <= i & i <= len q ) by A7, X, FINSEQ_1:3;
then ( 1 <= i & i < len M ) by A4, NAT_1:13;
hence (Del M,(len M)) . i = M . i by A1, A3, A9, FINSEQ_3:119
.= q . i by A2, A8, FINSEQ_1:def 7 ;
:: thesis: verum

end;

hence M = (Del M,(len M)) ^ <*(M . (len M))*> by A2, A5, A6, FINSEQ_2:10; :: thesis: verum