let x be bound_QC-variable; :: thesis: for A being non empty set
for v being Element of Valuations_in A
for S being Element of CQC-Sub-WFF
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 A
for S being Element of CQC-Sub-WFF
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 A; :: thesis: for S being Element of CQC-Sub-WFF
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 ; :: 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 ,A by VALUAT_1:def 1;
then ex f being Function st
( v = f & dom f = bound_QC-variables & 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:46;
v . ((S_Bound (@ (CQCSub_All [S,x],xSQ))) | a) is Element of Funcs bound_QC-variables ,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 & 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:46;
for b being set 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 set ; :: 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:12;
then reconsider x = (@ (RestrictSub x,(All x,(S `1 )),xSQ)) . b as bound_QC-variable ;
not S_Bound (@ (CQCSub_All [S,x],xSQ)) in rng (RestrictSub x,(All x,(S `1 )),xSQ) by A1, Th41;
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 Th49;
(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:22;
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:22; :: 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:9, RELAT_1:46; :: thesis: verum