for Al being QC-alphabet
for f being FinSequence of CQC-WFF Al
for P being Permutation of (dom f) holds dom (Per (f,P)) = dom f