theorem :: SUBSTUT2:20

for Al being QC-alphabet
for p, q being Element of CQC-WFF Al
for x, y being bound_QC-variable of Al holds
( (p '&' q) . (x,y) = (p . (x,y)) '&' (q . (x,y)) & ( QuantNbr p = QuantNbr (p . (x,y)) & QuantNbr q = QuantNbr (q . (x,y)) implies QuantNbr (p '&' q) = QuantNbr ((p '&' q) . (x,y)) ) )