for Al being QC-alphabet
for f being FinSequence of CQC-WFF Al holds still_not-bound_in f = union { (still_not-bound_in p) where p is Element of CQC-WFF Al : ex i being Nat st
( i in dom f & p = f . i ) }