let M be FinSequence; :: thesis: ( M <> {} implies M = (Del (M,(len M))) ^ <*(M . (len M))*> )
assume M <> {} ; :: thesis: M = (Del (M,(len M))) ^ <*(M . (len M))*>
then consider q being FinSequence, x being object such that
A1: M = q ^ <*x*> by FINSEQ_1:46;
A2: len M = (len q) + (len <*x*>) by A1, FINSEQ_1:22
.= (len q) + 1 by FINSEQ_1:39 ;
then A3: len (Del (M,(len M))) = len q by Th11;
A4: dom q = Seg (len q) by FINSEQ_1:def 3;
A5: now :: thesis: for i being Nat st i in dom q holds
(Del (M,(len M))) . i = q . i
let i be Nat; :: thesis: ( i in dom q implies (Del (M,(len M))) . i = q . i )
assume A6: i in dom q ; :: thesis: (Del (M,(len M))) . i = q . i
then i <= len q by A4, FINSEQ_1:1;
then ( i in NAT & i < len M ) by A2, NAT_1:13, ORDINAL1:def 12;
hence (Del (M,(len M))) . i = M . i by FINSEQ_3:110
.= q . i by A1, A6, FINSEQ_1:def 7 ;
:: thesis: verum
end;
M . (len M) = x by A1, A2, FINSEQ_1:42;
hence M = (Del (M,(len M))) ^ <*(M . (len M))*> by A1, A3, A5, FINSEQ_2:9; :: thesis: verum