theorem Th20: :: CALCUL_2:20

for Al being QC-alphabet
for p being Element of CQC-WFF Al
for f, g being FinSequence of CQC-WFF Al st |- f ^ <*p*> holds
|- (g ^ f) ^ <*p*>