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 a being Element of A
for X being set st X c= bound_QC-variables Al & not x in X holds
(v . (x | a)) | X = v | X