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

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