let Al be QC-alphabet ; :: thesis: for f being FinSequence of CQC-WFF Al st len f > 0 holds
( f = (Ant f) ^ <*(Suc f)*> & rng f = (rng (Ant f)) \/ {(Suc f)} )

let f be FinSequence of CQC-WFF Al; :: 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;
A3: dom f = Seg (len f) by FINSEQ_1:def 3;
A4: now :: thesis: for j being Nat st j in dom f holds
f . j = ((Ant f) ^ <*(Suc f)*>) . j
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 by ;
A7: now :: thesis: ( j <= len (Ant f) implies f . j = ((Ant f) ^ <*(Suc f)*>) . j )
assume j <= len (Ant f) ; :: thesis: f . j = ((Ant f) ^ <*(Suc f)*>) . j
then A8: j in dom (Ant f) by ;
Ant f = f | (Seg (len (Ant f))) by ;
then Ant f = f | (dom (Ant f)) by FINSEQ_1:def 3;
then f . j = (Ant f) . j by ;
hence f . j = ((Ant f) ^ <*(Suc f)*>) . j by ; :: thesis: verum
end;
A9: now :: thesis: ( j = (len (Ant f)) + 1 implies f . j = ((Ant f) ^ <*(Suc f)*>) . j )
1 in Seg 1 by FINSEQ_1:1;
then A10: 1 in dom <*(Suc f)*> by FINSEQ_1:38;
assume A11: j = (len (Ant f)) + 1 ; :: thesis: f . j = ((Ant f) ^ <*(Suc f)*>) . j
then j = len f by ;
then f . j = Suc f by ;
then f . j = <*(Suc f)*> . 1 by FINSEQ_1:40;
hence f . j = ((Ant f) ^ <*(Suc f)*>) . j by ; :: thesis: verum
end;
j <= (len (Ant f)) + 1 by ;
hence f . j = ((Ant f) ^ <*(Suc f)*>) . j by ; :: thesis: verum
end;
len f = (len (Ant f)) + (len <*(Suc f)*>) by ;
then A12: len f = len ((Ant f) ^ <*(Suc f)*>) by FINSEQ_1:22;
then f = (Ant f) ^ <*(Suc f)*> by ;
then rng f = (rng (Ant f)) \/ (rng <*(Suc f)*>) by FINSEQ_1:31;
hence ( f = (Ant f) ^ <*(Suc f)*> & rng f = (rng (Ant f)) \/ {(Suc f)} ) by ; :: thesis: verum