let Al be QC-alphabet ; 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; 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; ( ( 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])
; 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; 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; verum