theorem Th16: :: CALCUL_2:16

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