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