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) )
set Z = [(All x,(S `1 )),xSQ];
set q = All x,(S `1 );
assume [S,x] is quantifiable ; :: thesis: S `2 = ExpandSub x,(S `1 ),(RestrictSub x,(All x,(S `1 )),xSQ)
then A1: ([S,x] `1 ) `2 = QSub . [(All ([S,x] `2 ),(([S,x] `1 ) `1 )),xSQ] by SUBSTUT1:def 23;
[(All ([S,x] `2 ),(([S,x] `1 ) `1 )),xSQ] = [(All x,(([S,x] `1 ) `1 )),xSQ] by MCART_1:7;
then A2: [(All ([S,x] `2 ),(([S,x] `1 ) `1 )),xSQ] = [(All x,(S `1 )),xSQ] by MCART_1:7;
[(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 A1, A2, 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
A3: [[(All x,(S `1 )),xSQ],(S `2 )] = [[p,Sub1],b] and
A4: p,Sub1 PQSub b by SUBSTUT1:def 15;
[(All x,(S `1 )),xSQ] = [p,Sub1] by A3, ZFMISC_1:33;
then A5: ( All x,(S `1 ) = p & xSQ = Sub1 ) by ZFMISC_1:33;
A6: All x,(S `1 ) is universal by QC_LANG1:def 20;
then A7: bound_in (All x,(S `1 )) = x by QC_LANG1:def 26;
S `2 = b by A3, ZFMISC_1:33;
then 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;
hence S `2 = ExpandSub x,(S `1 ),(RestrictSub x,(All x,(S `1 )),xSQ) by A6, A7, QC_LANG1:def 27; :: thesis: verum