theorem Th25: :: CQC_LANG:25

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