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] holds dom (NEx_Val (v,S,x,xSQ)) = dom (RestrictSub (x,(All (x,(S `1))),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] 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 (Al,A)
for S being Element of CQC-Sub-WFF Al
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 (Al,A); :: thesis: for S being Element of CQC-Sub-WFF Al
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 Al; :: 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 Al ;
then rng (@ (RestrictSub (x,(All (x,(S `1))),xSQ))) c= dom v by Th58;
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