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