let Al be QC-alphabet ; :: thesis: for x being bound_QC-variable of Al
for A being non empty set
for v being Element of Valuations_in (Al,A)
for S being Element of CQC-Sub-WFF Al
for xSQ being second_Q_comp of [S,x] st [S,x] is quantifiable holds
for a being Element of A holds NEx_Val ((v . ((S_Bound (@ (CQCSub_All ([S,x],xSQ)))) | a)),S,x,xSQ) = NEx_Val (v,S,x,xSQ)
let x be bound_QC-variable of Al; :: thesis: for A being non empty set
for v being Element of Valuations_in (Al,A)
for S being Element of CQC-Sub-WFF Al
for xSQ being second_Q_comp of [S,x] st [S,x] is quantifiable holds
for a being Element of A holds NEx_Val ((v . ((S_Bound (@ (CQCSub_All ([S,x],xSQ)))) | a)),S,x,xSQ) = NEx_Val (v,S,x,xSQ)
let A be non empty set ; :: thesis: for v being Element of Valuations_in (Al,A)
for S being Element of CQC-Sub-WFF Al
for xSQ being second_Q_comp of [S,x] st [S,x] is quantifiable holds
for a being Element of A holds NEx_Val ((v . ((S_Bound (@ (CQCSub_All ([S,x],xSQ)))) | a)),S,x,xSQ) = NEx_Val (v,S,x,xSQ)
let v be Element of Valuations_in (Al,A); :: 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
for a being Element of A holds NEx_Val ((v . ((S_Bound (@ (CQCSub_All ([S,x],xSQ)))) | a)),S,x,xSQ) = NEx_Val (v,S,x,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
for a being Element of A holds NEx_Val ((v . ((S_Bound (@ (CQCSub_All ([S,x],xSQ)))) | a)),S,x,xSQ) = NEx_Val (v,S,x,xSQ)
let xSQ be second_Q_comp of [S,x]; :: thesis: ( [S,x] is quantifiable implies for a being Element of A holds NEx_Val ((v . ((S_Bound (@ (CQCSub_All ([S,x],xSQ)))) | a)),S,x,xSQ) = NEx_Val (v,S,x,xSQ) )
assume A1: [S,x] is quantifiable ; :: thesis: for a being Element of A holds NEx_Val ((v . ((S_Bound (@ (CQCSub_All ([S,x],xSQ)))) | a)),S,x,xSQ) = NEx_Val (v,S,x,xSQ)
set finSub = RestrictSub (x,(All (x,(S `1))),xSQ);
set NF1 = NEx_Val (v,S,x,xSQ);
set S1 = CQCSub_All ([S,x],xSQ);
let a be Element of A; :: thesis: NEx_Val ((v . ((S_Bound (@ (CQCSub_All ([S,x],xSQ)))) | a)),S,x,xSQ) = NEx_Val (v,S,x,xSQ)
set z = S_Bound (@ (CQCSub_All ([S,x],xSQ)));
set NF = NEx_Val ((v . ((S_Bound (@ (CQCSub_All ([S,x],xSQ)))) | a)),S,x,xSQ);
v is Element of Funcs ((bound_QC-variables Al),A) by VALUAT_1:def 1;
then ex f being Function st
( v = f & dom f = bound_QC-variables Al & rng f c= A ) by FUNCT_2:def 2;
then rng (@ (RestrictSub (x,(All (x,(S `1))),xSQ))) c= dom v ;
then A2: dom (NEx_Val (v,S,x,xSQ)) = dom (@ (RestrictSub (x,(All (x,(S `1))),xSQ))) by RELAT_1:27;
v . ((S_Bound (@ (CQCSub_All ([S,x],xSQ)))) | a) is Element of Funcs ((bound_QC-variables Al),A) by VALUAT_1:def 1;
then ex f being Function st
( v . ((S_Bound (@ (CQCSub_All ([S,x],xSQ)))) | a) = f & dom f = bound_QC-variables Al & rng f c= A ) by FUNCT_2:def 2;
then A3: rng (@ (RestrictSub (x,(All (x,(S `1))),xSQ))) c= dom (v . ((S_Bound (@ (CQCSub_All ([S,x],xSQ)))) | a)) ;
then A4: dom (NEx_Val ((v . ((S_Bound (@ (CQCSub_All ([S,x],xSQ)))) | a)),S,x,xSQ)) = dom (@ (RestrictSub (x,(All (x,(S `1))),xSQ))) by RELAT_1:27;
for b being object st b in dom (NEx_Val ((v . ((S_Bound (@ (CQCSub_All ([S,x],xSQ)))) | a)),S,x,xSQ)) holds
(NEx_Val ((v . ((S_Bound (@ (CQCSub_All ([S,x],xSQ)))) | a)),S,x,xSQ)) . b = (NEx_Val (v,S,x,xSQ)) . b

proof

let b be object ; :: thesis: ( b in dom (NEx_Val ((v . ((S_Bound (@ (CQCSub_All ([S,x],xSQ)))) | a)),S,x,xSQ)) implies (NEx_Val ((v . ((S_Bound (@ (CQCSub_All ([S,x],xSQ)))) | a)),S,x,xSQ)) . b = (NEx_Val (v,S,x,xSQ)) . b )
assume A5: b in dom (NEx_Val ((v . ((S_Bound (@ (CQCSub_All ([S,x],xSQ)))) | a)),S,x,xSQ)) ; :: thesis: (NEx_Val ((v . ((S_Bound (@ (CQCSub_All ([S,x],xSQ)))) | a)),S,x,xSQ)) . b = (NEx_Val (v,S,x,xSQ)) . b
A6: (@ (RestrictSub (x,(All (x,(S `1))),xSQ))) . b in rng (@ (RestrictSub (x,(All (x,(S `1))),xSQ))) by A4, A5, FUNCT_1:3;
then reconsider x = (@ (RestrictSub (x,(All (x,(S `1))),xSQ))) . b as bound_QC-variable of Al ;
not S_Bound (@ (CQCSub_All ([S,x],xSQ))) in rng (RestrictSub (x,(All (x,(S `1))),xSQ)) by A1, Th40;
then S_Bound (@ (CQCSub_All ([S,x],xSQ))) <> x by A6, SUBSTUT1:def 2;
then A7: (v . ((S_Bound (@ (CQCSub_All ([S,x],xSQ)))) | a)) . x = v . x by Th48;
(NEx_Val ((v . ((S_Bound (@ (CQCSub_All ([S,x],xSQ)))) | a)),S,x,xSQ)) . b = (v . ((S_Bound (@ (CQCSub_All ([S,x],xSQ)))) | a)) . x by A5, FUNCT_1:12;
hence (NEx_Val ((v . ((S_Bound (@ (CQCSub_All ([S,x],xSQ)))) | a)),S,x,xSQ)) . b = (NEx_Val (v,S,x,xSQ)) . b by A4, A2, A5, A7, FUNCT_1:12; :: thesis: verum

end;

hence NEx_Val ((v . ((S_Bound (@ (CQCSub_All ([S,x],xSQ)))) | a)),S,x,xSQ) = NEx_Val (v,S,x,xSQ) by A3, A2, FUNCT_1:2, RELAT_1:27; :: thesis: verum