let Al be QC-alphabet ; :: thesis: for x being bound_QC-variable of Al
for S being Element of CQC-Sub-WFF Al
for xSQ being second_Q_comp of [S,x] st [S,x] is quantifiable holds
CQCQuant ((CQCSub_All ([S,x],xSQ)),(CQC_Sub S)) = All ((S_Bound (@ (CQCSub_All ([S,x],xSQ)))),(CQC_Sub S))
let x be bound_QC-variable of Al; :: thesis: for S being Element of CQC-Sub-WFF Al
for xSQ being second_Q_comp of [S,x] st [S,x] is quantifiable holds
CQCQuant ((CQCSub_All ([S,x],xSQ)),(CQC_Sub S)) = All ((S_Bound (@ (CQCSub_All ([S,x],xSQ)))),(CQC_Sub S))
let S be Element of CQC-Sub-WFF Al; :: thesis: for xSQ being second_Q_comp of [S,x] st [S,x] is quantifiable holds
CQCQuant ((CQCSub_All ([S,x],xSQ)),(CQC_Sub S)) = All ((S_Bound (@ (CQCSub_All ([S,x],xSQ)))),(CQC_Sub S))
let xSQ be second_Q_comp of [S,x]; :: thesis: ( [S,x] is quantifiable implies CQCQuant ((CQCSub_All ([S,x],xSQ)),(CQC_Sub S)) = All ((S_Bound (@ (CQCSub_All ([S,x],xSQ)))),(CQC_Sub S)) )
set S1 = CQCSub_All ([S,x],xSQ);
set p = CQC_Sub (CQCSub_the_scope_of (CQCSub_All ([S,x],xSQ)));
A1: Quant ((CQCSub_All ([S,x],xSQ)),(CQC_Sub (CQCSub_the_scope_of (CQCSub_All ([S,x],xSQ))))) = All ((S_Bound (@ (CQCSub_All ([S,x],xSQ)))),(CQC_Sub (CQCSub_the_scope_of (CQCSub_All ([S,x],xSQ))))) by SUBSTUT1:def 37;
assume A2: [S,x] is quantifiable ; :: thesis: CQCQuant ((CQCSub_All ([S,x],xSQ)),(CQC_Sub S)) = All ((S_Bound (@ (CQCSub_All ([S,x],xSQ)))),(CQC_Sub S))
then CQCSub_All ([S,x],xSQ) = Sub_All ([S,x],xSQ) by Def5;
then CQCSub_All ([S,x],xSQ) is Sub_universal by A2, SUBSTUT1:14;
then A3: CQCQuant ((CQCSub_All ([S,x],xSQ)),(CQC_Sub (CQCSub_the_scope_of (CQCSub_All ([S,x],xSQ))))) = Quant ((CQCSub_All ([S,x],xSQ)),(CQC_Sub (CQCSub_the_scope_of (CQCSub_All ([S,x],xSQ))))) by Def7;
CQCQuant ((CQCSub_All ([S,x],xSQ)),(CQC_Sub S)) = CQCQuant ((CQCSub_All ([S,x],xSQ)),(CQC_Sub (CQCSub_the_scope_of (CQCSub_All ([S,x],xSQ))))) by A2, Th30;
hence CQCQuant ((CQCSub_All ([S,x],xSQ)),(CQC_Sub S)) = All ((S_Bound (@ (CQCSub_All ([S,x],xSQ)))),(CQC_Sub S)) by A2, A3, A1, Th30; :: thesis: verum