theorem :: CQC_THE2:14

for A being QC-alphabet
for p being Element of CQC-WFF A
for x, y being bound_QC-variable of A st x <> y holds
(Ex (x,p)) . y = Ex (x,(p . y))