let Al be QC-alphabet ; :: thesis: for p being Element of CQC-WFF Al

for x being bound_QC-variable of Al st ( for Sub being CQC_Substitution of Al holds QuantNbr p = QuantNbr (CQC_Sub [p,Sub]) ) holds

for Sub being CQC_Substitution of Al holds QuantNbr (All (x,p)) = QuantNbr (CQC_Sub [(All (x,p)),Sub])

let p be Element of CQC-WFF Al; :: thesis: for x being bound_QC-variable of Al st ( for Sub being CQC_Substitution of Al holds QuantNbr p = QuantNbr (CQC_Sub [p,Sub]) ) holds

for Sub being CQC_Substitution of Al holds QuantNbr (All (x,p)) = QuantNbr (CQC_Sub [(All (x,p)),Sub])

let x be bound_QC-variable of Al; :: thesis: ( ( for Sub being CQC_Substitution of Al holds QuantNbr p = QuantNbr (CQC_Sub [p,Sub]) ) implies for Sub being CQC_Substitution of Al holds QuantNbr (All (x,p)) = QuantNbr (CQC_Sub [(All (x,p)),Sub]) )

assume A1: for Sub being CQC_Substitution of Al holds QuantNbr p = QuantNbr (CQC_Sub [p,Sub]) ; :: thesis: for Sub being CQC_Substitution of Al holds QuantNbr (All (x,p)) = QuantNbr (CQC_Sub [(All (x,p)),Sub])

let Sub be CQC_Substitution of Al; :: thesis: QuantNbr (All (x,p)) = QuantNbr (CQC_Sub [(All (x,p)),Sub])

set S1 = [(All (x,p)),Sub];

set S = [p,((CFQ Al) . [(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 Al) . [(All (x,p)),Sub])],x] `1 by A2, SUBSTUT1:21

.= [p,((CFQ Al) . [(All (x,p)),Sub])] ;

then CQC_Sub [(All (x,p)),Sub] = CQCQuant ((CQCSub_All ((QScope (p,x,Sub)),(Qsc (p,x,Sub)))),(CQC_Sub [p,((CFQ Al) . [(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 Al) . [(All (x,p)),Sub])]))) by Th22, SUBLEMMA:31

.= (QuantNbr (CQC_Sub [p,((CFQ Al) . [(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

for x being bound_QC-variable of Al st ( for Sub being CQC_Substitution of Al holds QuantNbr p = QuantNbr (CQC_Sub [p,Sub]) ) holds

for Sub being CQC_Substitution of Al holds QuantNbr (All (x,p)) = QuantNbr (CQC_Sub [(All (x,p)),Sub])

let p be Element of CQC-WFF Al; :: thesis: for x being bound_QC-variable of Al st ( for Sub being CQC_Substitution of Al holds QuantNbr p = QuantNbr (CQC_Sub [p,Sub]) ) holds

for Sub being CQC_Substitution of Al holds QuantNbr (All (x,p)) = QuantNbr (CQC_Sub [(All (x,p)),Sub])

let x be bound_QC-variable of Al; :: thesis: ( ( for Sub being CQC_Substitution of Al holds QuantNbr p = QuantNbr (CQC_Sub [p,Sub]) ) implies for Sub being CQC_Substitution of Al holds QuantNbr (All (x,p)) = QuantNbr (CQC_Sub [(All (x,p)),Sub]) )

assume A1: for Sub being CQC_Substitution of Al holds QuantNbr p = QuantNbr (CQC_Sub [p,Sub]) ; :: thesis: for Sub being CQC_Substitution of Al holds QuantNbr (All (x,p)) = QuantNbr (CQC_Sub [(All (x,p)),Sub])

let Sub be CQC_Substitution of Al; :: thesis: QuantNbr (All (x,p)) = QuantNbr (CQC_Sub [(All (x,p)),Sub])

set S1 = [(All (x,p)),Sub];

set S = [p,((CFQ Al) . [(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 Al) . [(All (x,p)),Sub])],x] `1 by A2, SUBSTUT1:21

.= [p,((CFQ Al) . [(All (x,p)),Sub])] ;

then CQC_Sub [(All (x,p)),Sub] = CQCQuant ((CQCSub_All ((QScope (p,x,Sub)),(Qsc (p,x,Sub)))),(CQC_Sub [p,((CFQ Al) . [(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 Al) . [(All (x,p)),Sub])]))) by Th22, SUBLEMMA:31

.= (QuantNbr (CQC_Sub [p,((CFQ Al) . [(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