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
S `2 = ExpandSub (x,(S `1),(RestrictSub (x,(All (x,(S `1))),xSQ)))
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
S `2 = ExpandSub (x,(S `1),(RestrictSub (x,(All (x,(S `1))),xSQ)))
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
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 Al) . [(All (([S,x] `2),(([S,x] `1) `1))),xSQ] by SUBSTUT1:def 23;
A2: [(All (x,(S `1))),xSQ] in [:(QC-WFF Al),(vSUB Al):] by ZFMISC_1:def 2;
[:(QC-WFF Al),(vSUB Al):] c= dom (QSub Al) by Th34;
then [[(All (x,(S `1))),xSQ],(([S,x] `1) `2)] in QSub Al by A2, A1, FUNCT_1:1;
then [[(All (x,(S `1))),xSQ],(S `2)] in QSub Al ;
then consider p being QC-formula of Al, Sub1 being CQC_Substitution of Al, 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, XTUPLE_0:1;
then A5: ( All (x,(S `1)) = p & xSQ = Sub1 ) by XTUPLE_0:1;
A6: All (x,(S `1)) is universal by QC_LANG1:def 21;
then A7: bound_in (All (x,(S `1))) = x by QC_LANG1:def 27;
S `2 = b by A3, XTUPLE_0:1;
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 28; :: thesis: verum