let k be Element of NAT ; :: thesis: for x, y being bound_QC-variable
for P being QC-pred_symbol of k
for l being CQC-variable_list of 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; :: thesis: for P being QC-pred_symbol of k
for l being CQC-variable_list of 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; :: thesis: for l being CQC-variable_list of 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 ; :: 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:9;
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