:: deftheorem Def2 defines Suc CALCUL_1:def 2 :
for Al being QC-alphabet
for f being FinSequence of CQC-WFF Al holds
( ( len f > 0 implies Suc f = f . (len f) ) & ( not len f > 0 implies Suc f = VERUM Al ) );