theorem Th24: :: SUBSTUT2:24

for Al being QC-alphabet
for Sub being CQC_Substitution of Al holds QuantNbr (VERUM Al) = QuantNbr (CQC_Sub [(VERUM Al),Sub])