let Al be QC-alphabet ; :: thesis: for k being Nat

for x, y being bound_QC-variable of Al

for P being QC-pred_symbol of k,Al

for l being CQC-variable_list of k,Al holds

( (P ! l) . (x,y) = P ! (CQC_Subst (l,(Sbst (x,y)))) & QuantNbr (P ! l) = QuantNbr ((P ! l) . (x,y)) )

let k be Nat; :: thesis: for x, y being bound_QC-variable of Al

for P being QC-pred_symbol of k,Al

for l being CQC-variable_list of k,Al holds

( (P ! l) . (x,y) = P ! (CQC_Subst (l,(Sbst (x,y)))) & QuantNbr (P ! l) = QuantNbr ((P ! l) . (x,y)) )

let x, y be bound_QC-variable of Al; :: thesis: for P being QC-pred_symbol of k,Al

for l being CQC-variable_list of k,Al holds

( (P ! l) . (x,y) = P ! (CQC_Subst (l,(Sbst (x,y)))) & QuantNbr (P ! l) = QuantNbr ((P ! l) . (x,y)) )

let P be QC-pred_symbol of k,Al; :: thesis: for l being CQC-variable_list of k,Al holds

( (P ! l) . (x,y) = P ! (CQC_Subst (l,(Sbst (x,y)))) & QuantNbr (P ! l) = QuantNbr ((P ! l) . (x,y)) )

let l be CQC-variable_list of k,Al; :: thesis: ( (P ! l) . (x,y) = P ! (CQC_Subst (l,(Sbst (x,y)))) & QuantNbr (P ! l) = QuantNbr ((P ! l) . (x,y)) )

set S = [(P ! l),(Sbst (x,y))];

[(P ! l),(Sbst (x,y))] = Sub_P (P,l,(Sbst (x,y))) by SUBSTUT1:9;

then A1: (P ! l) . (x,y) = P ! (CQC_Subst (l,(Sbst (x,y)))) by SUBLEMMA:8;

QuantNbr (P ! (CQC_Subst (l,(Sbst (x,y))))) = 0 by CQC_SIM1:15;

hence ( (P ! l) . (x,y) = P ! (CQC_Subst (l,(Sbst (x,y)))) & QuantNbr (P ! l) = QuantNbr ((P ! l) . (x,y)) ) by A1, CQC_SIM1:15; :: thesis: verum

for x, y being bound_QC-variable of Al

for P being QC-pred_symbol of k,Al

for l being CQC-variable_list of k,Al holds

( (P ! l) . (x,y) = P ! (CQC_Subst (l,(Sbst (x,y)))) & QuantNbr (P ! l) = QuantNbr ((P ! l) . (x,y)) )

let k be Nat; :: thesis: for x, y being bound_QC-variable of Al

for P being QC-pred_symbol of k,Al

for l being CQC-variable_list of k,Al holds

( (P ! l) . (x,y) = P ! (CQC_Subst (l,(Sbst (x,y)))) & QuantNbr (P ! l) = QuantNbr ((P ! l) . (x,y)) )

let x, y be bound_QC-variable of Al; :: thesis: for P being QC-pred_symbol of k,Al

for l being CQC-variable_list of k,Al holds

( (P ! l) . (x,y) = P ! (CQC_Subst (l,(Sbst (x,y)))) & QuantNbr (P ! l) = QuantNbr ((P ! l) . (x,y)) )

let P be QC-pred_symbol of k,Al; :: thesis: for l being CQC-variable_list of k,Al holds

( (P ! l) . (x,y) = P ! (CQC_Subst (l,(Sbst (x,y)))) & QuantNbr (P ! l) = QuantNbr ((P ! l) . (x,y)) )

let l be CQC-variable_list of k,Al; :: thesis: ( (P ! l) . (x,y) = P ! (CQC_Subst (l,(Sbst (x,y)))) & QuantNbr (P ! l) = QuantNbr ((P ! l) . (x,y)) )

set S = [(P ! l),(Sbst (x,y))];

[(P ! l),(Sbst (x,y))] = Sub_P (P,l,(Sbst (x,y))) by SUBSTUT1:9;

then A1: (P ! l) . (x,y) = P ! (CQC_Subst (l,(Sbst (x,y)))) by SUBLEMMA:8;

QuantNbr (P ! (CQC_Subst (l,(Sbst (x,y))))) = 0 by CQC_SIM1:15;

hence ( (P ! l) . (x,y) = P ! (CQC_Subst (l,(Sbst (x,y)))) & QuantNbr (P ! l) = QuantNbr ((P ! l) . (x,y)) ) by A1, CQC_SIM1:15; :: thesis: verum