let k be Element of NAT ; :: thesis: for P being QC-pred_symbol of k
for l being CQC-variable_list of k
for Sub being CQC_Substitution holds QuantNbr (P ! l) = QuantNbr (CQC_Sub [(P ! l),Sub])
let P be QC-pred_symbol of k; :: thesis: for l being CQC-variable_list of k
for Sub being CQC_Substitution holds QuantNbr (P ! l) = QuantNbr (CQC_Sub [(P ! l),Sub])
let l be CQC-variable_list of k; :: thesis: for Sub being CQC_Substitution holds QuantNbr (P ! l) = QuantNbr (CQC_Sub [(P ! l),Sub])
let Sub be CQC_Substitution; :: 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