theorem :: SUBSTUT2:25

for Al being QC-alphabet
for p being Element of CQC-WFF Al
for Sub being CQC_Substitution of Al holds QuantNbr p = QuantNbr (CQC_Sub [p,Sub])