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