theorem :: CALCUL_1:61

for Al being QC-alphabet
for p, q being Element of CQC-WFF Al
for x, y being bound_QC-variable of Al
for f being FinSequence of CQC-WFF Al st |- (f ^ <*(p . (x,y))*>) ^ <*q*> & not y in still_not-bound_in ((f ^ <*(Ex (x,p))*>) ^ <*q*>) holds
|- (f ^ <*(Ex (x,p))*>) ^ <*q*>