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:27;
hence dom (NEx_Val (v,S,x,xSQ)) = dom (RestrictSub (x,(All (x,(S `1))),xSQ)) by SUBSTUT1:def 2; :: thesis: verum