let p be Element of CQC-WFF ; :: thesis: for x being bound_QC-variable st ( for Sub being CQC_Substitution holds QuantNbr p = QuantNbr (CQC_Sub [p,Sub]) ) holds
for Sub being CQC_Substitution holds QuantNbr (All x,p) = QuantNbr (CQC_Sub [(All x,p),Sub])
let x be bound_QC-variable; :: thesis: ( ( for Sub being CQC_Substitution holds QuantNbr p = QuantNbr (CQC_Sub [p,Sub]) ) implies for Sub being CQC_Substitution holds QuantNbr (All x,p) = QuantNbr (CQC_Sub [(All x,p),Sub]) )
assume A1: for Sub being CQC_Substitution holds QuantNbr p = QuantNbr (CQC_Sub [p,Sub]) ; :: thesis: for Sub being CQC_Substitution holds QuantNbr (All x,p) = QuantNbr (CQC_Sub [(All x,p),Sub])
let Sub be CQC_Substitution; :: thesis: QuantNbr (All x,p) = QuantNbr (CQC_Sub [(All x,p),Sub])
set S1 = [(All x,p),Sub];
set S = [p,(CFQ . [(All x,p),Sub])];
A2: QScope p,x,Sub is quantifiable by Th22;
A3: Sub_All (QScope p,x,Sub),(Qsc p,x,Sub) = CQCSub_All (QScope p,x,Sub),(Qsc p,x,Sub) by SUBLEMMA:def 6, Th22
.= [(All x,p),Sub] by Th22 ;
then A4: [(All x,p),Sub] is Sub_universal by A2, SUBSTUT1:def 28;
then A5: CQC_Sub [(All x,p),Sub] = CQCQuant [(All x,p),Sub],(CQC_Sub (CQCSub_the_scope_of [(All x,p),Sub])) by SUBLEMMA:29;
CQCSub_the_scope_of [(All x,p),Sub] = Sub_the_scope_of (Sub_All (QScope p,x,Sub),(Qsc p,x,Sub)) by A3, A4, SUBLEMMA:def 7
.= [[p,(CFQ . [(All x,p),Sub])],x] `1 by A2, SUBSTUT1:21
.= [p,(CFQ . [(All x,p),Sub])] by MCART_1:7 ;
then A6: CQC_Sub [(All x,p),Sub] = CQCQuant (CQCSub_All (QScope p,x,Sub),(Qsc p,x,Sub)),(CQC_Sub [p,(CFQ . [(All x,p),Sub])]) by A5, Th22;
set y = S_Bound (@ (CQCSub_All (QScope p,x,Sub),(Qsc p,x,Sub)));
QuantNbr (CQC_Sub [(All x,p),Sub]) = QuantNbr (All (S_Bound (@ (CQCSub_All (QScope p,x,Sub),(Qsc p,x,Sub)))),(CQC_Sub [p,(CFQ . [(All x,p),Sub])])) by Th22, A6, SUBLEMMA:32
.= (QuantNbr (CQC_Sub [p,(CFQ . [(All x,p),Sub])])) + 1 by CQC_SIM1:18
.= (QuantNbr p) + 1 by A1 ;
hence QuantNbr (All x,p) = QuantNbr (CQC_Sub [(All x,p),Sub]) by CQC_SIM1:18; :: thesis: verum