let Al be QC-alphabet ; :: thesis: for k being Nat
for P being QC-pred_symbol of k,Al
for l being CQC-variable_list of k,Al
for Sub being CQC_Substitution of Al holds QuantNbr (P ! l) = QuantNbr (CQC_Sub [(P ! l),Sub])
let k be Nat; :: thesis: for P being QC-pred_symbol of k,Al
for l being CQC-variable_list of k,Al
for Sub being CQC_Substitution of Al holds QuantNbr (P ! l) = QuantNbr (CQC_Sub [(P ! l),Sub])
let P be QC-pred_symbol of k,Al; :: thesis: for l being CQC-variable_list of k,Al
for Sub being CQC_Substitution of Al holds QuantNbr (P ! l) = QuantNbr (CQC_Sub [(P ! l),Sub])
let l be CQC-variable_list of k,Al; :: thesis: for Sub being CQC_Substitution of Al holds QuantNbr (P ! l) = QuantNbr (CQC_Sub [(P ! l),Sub])
let Sub be CQC_Substitution of Al; :: thesis: QuantNbr (P ! l) = QuantNbr (CQC_Sub [(P ! l),Sub])
set S = [(P ! l),Sub];
[(P ! l),Sub] = Sub_P (P,l,Sub) by SUBSTUT1:9;
then A1: CQC_Sub [(P ! l),Sub] = P ! (CQC_Subst (l,Sub)) by SUBLEMMA:8;
QuantNbr (P ! (CQC_Subst (l,Sub))) = 0 by CQC_SIM1:15;
hence QuantNbr (P ! l) = QuantNbr (CQC_Sub [(P ! l),Sub]) by A1, CQC_SIM1:15; :: thesis: verum