let x be bound_QC-variable; :: thesis: for S being Element of CQC-Sub-WFF
for xSQ being second_Q_comp of [S,x] st [S,x] is quantifiable holds
S `2 = ExpandSub x,(S `1 ),(RestrictSub x,(All x,(S `1 )),xSQ)
let S be Element of CQC-Sub-WFF ; :: thesis: for xSQ being second_Q_comp of [S,x] st [S,x] is quantifiable holds
S `2 = ExpandSub x,(S `1 ),(RestrictSub x,(All x,(S `1 )),xSQ)
let xSQ be second_Q_comp of [S,x]; :: thesis: ( [S,x] is quantifiable implies S `2 = ExpandSub x,(S `1 ),(RestrictSub x,(All x,(S `1 )),xSQ) )
assume A1: [S,x] is quantifiable ; :: thesis: S `2 = ExpandSub x,(S `1 ),(RestrictSub x,(All x,(S `1 )),xSQ)
A2: ([S,x] `1 ) `2 = QSub . [(All ([S,x] `2 ),(([S,x] `1 ) `1 )),xSQ] by A1, SUBSTUT1:def 23;
[(All ([S,x] `2 ),(([S,x] `1 ) `1 )),xSQ] = [(All x,(([S,x] `1 ) `1 )),xSQ] by MCART_1:7;
then A3: [(All ([S,x] `2 ),(([S,x] `1 ) `1 )),xSQ] = [(All x,(S `1 )),xSQ] by MCART_1:7;
set Z = [(All x,(S `1 )),xSQ];
[(All x,(S `1 )),xSQ] in [:QC-WFF ,vSUB :] by ZFMISC_1:def 2;
then [[(All x,(S `1 )),xSQ],(([S,x] `1 ) `2 )] in QSub by A2, A3, Th35, FUNCT_1:8;
then [[(All x,(S `1 )),xSQ],(S `2 )] in QSub by MCART_1:7;
then consider p being QC-formula, Sub1 being CQC_Substitution, b being set such that
A4: ( [[(All x,(S `1 )),xSQ],(S `2 )] = [[p,Sub1],b] & p,Sub1 PQSub b ) by SUBSTUT1:def 15;
A5: ( [(All x,(S `1 )),xSQ] = [p,Sub1] & S `2 = b ) by A4, ZFMISC_1:33;
then A6: ( All x,(S `1 ) = p & xSQ = Sub1 ) by ZFMISC_1:33;
set q = All x,(S `1 );
A7: All x,(S `1 ) is universal by QC_LANG1:def 20;
then A8: S `2 = ExpandSub (bound_in (All x,(S `1 ))),(the_scope_of (All x,(S `1 ))),(RestrictSub (bound_in (All x,(S `1 ))),(All x,(S `1 )),xSQ) by A4, A5, A6, SUBSTUT1:def 14;
bound_in (All x,(S `1 )) = x by A7, QC_LANG1:def 26;
hence S `2 = ExpandSub x,(S `1 ),(RestrictSub x,(All x,(S `1 )),xSQ) by A7, A8, QC_LANG1:def 27; :: thesis: verum