let f be FinSequence of CQC-WFF ; :: thesis: ( len f > 0 implies ( f = (Ant f) ^ <*(Suc f)*> & rng f = (rng (Ant f)) \/ {(Suc f)} ) )
assume A1: len f > 0 ; :: thesis: ( f = (Ant f) ^ <*(Suc f)*> & rng f = (rng (Ant f)) \/ {(Suc f)} )
then A2: len f = (len (Ant f)) + 1 by Th2;
then len f = (len (Ant f)) + (len <*(Suc f)*>) by FINSEQ_1:56;
then A3: len f = len ((Ant f) ^ <*(Suc f)*>) by FINSEQ_1:35;
X: dom f = Seg (len f) by FINSEQ_1:def 3;

A4: now

let j be Nat; :: thesis: ( j in dom f implies f . j = ((Ant f) ^ <*(Suc f)*>) . j )
assume A5: j in dom f ; :: thesis: f . j = ((Ant f) ^ <*(Suc f)*>) . j
A6: ( 1 <= j & j <= (len (Ant f)) + 1 ) by A2, A5, X, FINSEQ_1:3;

A7: now

assume j <= len (Ant f) ; :: thesis: f . j = ((Ant f) ^ <*(Suc f)*>) . j
then A8: j in dom (Ant f) by A6, FINSEQ_3:27;
Ant f = f | (Seg (len (Ant f))) by A2, Def1;
then Ant f = f | (dom (Ant f)) by FINSEQ_1:def 3;
then f . j = (Ant f) . j by A8, FUNCT_1:72;
hence f . j = ((Ant f) ^ <*(Suc f)*>) . j by A8, FINSEQ_1:def 7; :: thesis: verum

end;

now

assume A9: j = (len (Ant f)) + 1 ; :: thesis: f . j = ((Ant f) ^ <*(Suc f)*>) . j
then j = len f by A1, Th2;
then f . j = Suc f by A1, Def2;
then A10: f . j = <*(Suc f)*> . 1 by FINSEQ_1:57;
1 in Seg 1 by FINSEQ_1:3;
then 1 in dom <*(Suc f)*> by FINSEQ_1:55;
hence f . j = ((Ant f) ^ <*(Suc f)*>) . j by A9, A10, FINSEQ_1:def 7; :: thesis: verum

end;

hence f . j = ((Ant f) ^ <*(Suc f)*>) . j by A6, A7, NAT_1:8; :: thesis: verum

end;

then f = (Ant f) ^ <*(Suc f)*> by A3, FINSEQ_2:10;
then rng f = (rng (Ant f)) \/ (rng <*(Suc f)*>) by FINSEQ_1:44;
hence ( f = (Ant f) ^ <*(Suc f)*> & rng f = (rng (Ant f)) \/ {(Suc f)} ) by A3, A4, FINSEQ_1:55, FINSEQ_2:10; :: thesis: verum