let Al be QC-alphabet ; :: thesis: for Sub being CQC_Substitution of Al holds QuantNbr (VERUM Al) = QuantNbr (CQC_Sub [(VERUM Al),Sub])
let Sub be CQC_Substitution of Al; :: thesis: QuantNbr (VERUM Al) = QuantNbr (CQC_Sub [(VERUM Al),Sub])
[(VERUM Al),Sub] is Al -Sub_VERUM by SUBSTUT1:def 19;
hence QuantNbr (VERUM Al) = QuantNbr (CQC_Sub [(VERUM Al),Sub]) by SUBLEMMA:3; :: thesis: verum