theorem Th14: :: CALCUL_2:14

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