for Al being QC-alphabet
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 st not x in dom (S `2) holds
(v . (Val_S (v,S))) . x = v . x