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 vS being Val_Sub of A,Al
for vS1 being Function st ( for y being bound_QC-variable of Al st y in dom vS1 holds
vS1 . y = v . y ) & dom vS misses dom vS1 holds
for y being bound_QC-variable of Al st y in (dom vS1) \ {x} holds
(vS1 | ((dom vS1) \ {x})) . y = (v . vS) . y