theorem :: CALCUL_2:32

for Al being QC-alphabet
for p, q being Element of CQC-WFF Al
for f being FinSequence of CQC-WFF Al
for n being Nat st 1 <= n & |- (f ^ (IdFinS (p,n))) ^ <*q*> holds
|- (f ^ <*p*>) ^ <*q*>