let Al be QC-alphabet ; 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; 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; 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]; ( [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))
; 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; verum