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] holds dom (NEx_Val v,S,x,xSQ) = dom (RestrictSub x,(All x,(S `1 )),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] holds dom (NEx_Val v,S,x,xSQ) = dom (RestrictSub x,(All x,(S `1 )),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] holds dom (NEx_Val v,S,x,xSQ) = dom (RestrictSub x,(All x,(S `1 )),xSQ)
let S be Element of CQC-Sub-WFF ; :: thesis: for xSQ being second_Q_comp of [S,x] holds dom (NEx_Val v,S,x,xSQ) = dom (RestrictSub x,(All x,(S `1 )),xSQ)
let xSQ be second_Q_comp of [S,x]; :: thesis: dom (NEx_Val v,S,x,xSQ) = dom (RestrictSub x,(All x,(S `1 )),xSQ)
rng (@ (RestrictSub x,(All x,(S `1 )),xSQ)) c= bound_QC-variables ;
then rng (@ (RestrictSub x,(All x,(S `1 )),xSQ)) c= dom v by Th59;
then dom (NEx_Val v,S,x,xSQ) = dom (@ (RestrictSub x,(All x,(S `1 )),xSQ)) by RELAT_1:46;
hence dom (NEx_Val v,S,x,xSQ) = dom (RestrictSub x,(All x,(S `1 )),xSQ) by SUBSTUT1:def 2; :: thesis: verum