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 & x in rng (RestrictSub (x,(All (x,(S `1))),xSQ)) holds
S_Bound (@ (CQCSub_All ([S,x],xSQ))) = x. (upVar ((RestrictSub (x,(All (x,(S `1))),xSQ)),(S `1)))
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 & x in rng (RestrictSub (x,(All (x,(S `1))),xSQ)) holds
S_Bound (@ (CQCSub_All ([S,x],xSQ))) = x. (upVar ((RestrictSub (x,(All (x,(S `1))),xSQ)),(S `1)))
let S be Element of CQC-Sub-WFF Al; :: thesis: for xSQ being second_Q_comp of [S,x] st [S,x] is quantifiable & x in rng (RestrictSub (x,(All (x,(S `1))),xSQ)) holds
S_Bound (@ (CQCSub_All ([S,x],xSQ))) = x. (upVar ((RestrictSub (x,(All (x,(S `1))),xSQ)),(S `1)))
let xSQ be second_Q_comp of [S,x]; :: thesis: ( [S,x] is quantifiable & x in rng (RestrictSub (x,(All (x,(S `1))),xSQ)) implies S_Bound (@ (CQCSub_All ([S,x],xSQ))) = x. (upVar ((RestrictSub (x,(All (x,(S `1))),xSQ)),(S `1))) )
set S1 = CQCSub_All ([S,x],xSQ);
assume that
A1: [S,x] is quantifiable and
A2: x in rng (RestrictSub (x,(All (x,(S `1))),xSQ)) ; :: thesis: S_Bound (@ (CQCSub_All ([S,x],xSQ))) = x. (upVar ((RestrictSub (x,(All (x,(S `1))),xSQ)),(S `1)))
A3: CQCSub_All ([S,x],xSQ) = Sub_All ([S,x],xSQ) by A1, Def5;
then A4: (CQCSub_All ([S,x],xSQ)) `2 = xSQ by A1, Th26;
A5: (CQCSub_All ([S,x],xSQ)) `1 = All (([S,x] `2),(([S,x] `1) `1)) by A1, A3, Th26;
then A6: (CQCSub_All ([S,x],xSQ)) `1 = All (x,(([S,x] `1) `1)) ;
then A7: ( (CQCSub_All ([S,x],xSQ)) `1 = All (x,(S `1)) & x = bound_in ((CQCSub_All ([S,x],xSQ)) `1) ) by QC_LANG2:7;
set finSub = RestrictSub ((bound_in ((CQCSub_All ([S,x],xSQ)) `1)),((CQCSub_All ([S,x],xSQ)) `1),((CQCSub_All ([S,x],xSQ)) `2));
A8: @ (CQCSub_All ([S,x],xSQ)) = CQCSub_All ([S,x],xSQ) by SUBSTUT1:def 35;
(CQCSub_All ([S,x],xSQ)) `1 = All (x,(([S,x] `1) `1)) by A5;
then bound_in ((CQCSub_All ([S,x],xSQ)) `1) = x by QC_LANG2:7;
then bound_in ((CQCSub_All ([S,x],xSQ)) `1) in rng (RestrictSub ((bound_in ((CQCSub_All ([S,x],xSQ)) `1)),((CQCSub_All ([S,x],xSQ)) `1),((CQCSub_All ([S,x],xSQ)) `2))) by A2, A4, A6;
then S_Bound (@ (CQCSub_All ([S,x],xSQ))) = x. (upVar ((RestrictSub ((bound_in ((CQCSub_All ([S,x],xSQ)) `1)),((CQCSub_All ([S,x],xSQ)) `1),((CQCSub_All ([S,x],xSQ)) `2))),(the_scope_of ((CQCSub_All ([S,x],xSQ)) `1)))) by A8, SUBSTUT1:def 36;
hence S_Bound (@ (CQCSub_All ([S,x],xSQ))) = x. (upVar ((RestrictSub (x,(All (x,(S `1))),xSQ)),(S `1))) by A4, A7, QC_LANG2:7; :: thesis: verum