for Al being QC-alphabet
for f, g being FinSequence of CQC-WFF Al holds dom ((g ^ f) | (seq ((len g),(len f)))) = seq ((len g),(len f))