theorem Th3: :: CALCUL_1:3

for Al being QC-alphabet
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)} )