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])];
set y = S_Bound (@ (CQCSub_All ((QScope (p,x,Sub)),(Qsc (p,x,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 Th22, SUBLEMMA:def 5
.= [(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:28;
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 6
.= [[p,(CFQ . [(All (x,p)),Sub])],x] `1 by A2, SUBSTUT1:21
.= [p,(CFQ . [(All (x,p)),Sub])] by MCART_1:7 ;
then 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;
then 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, SUBLEMMA:31
.= (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