theorem Th21: :: CALCUL_2:21

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