for Al being QC-alphabet
for f being FinSequence of CQC-WFF Al holds still_not-bound_in f is finite