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 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;
A4: len M = (len q) + (len <*x*>) by A2, FINSEQ_1:35
.= (len q) + 1 by FINSEQ_1:56 ;
then A5: len (Del M,(len M)) = len q by Th3;
A6: dom q = Seg (len q) by FINSEQ_1:def 3;

A7: now

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

end;

M . (len M) = x by A2, A4, FINSEQ_1:59;
hence M = (Del M,(len M)) ^ <*(M . (len M))*> by A2, A5, A7, FINSEQ_2:10; :: thesis: verum