theorem :: VALUAT_1:26

for Al being QC-alphabet
for A being non empty set
for Y, Z being bound_QC-variable of Al
for V1, V2 being Element of Valuations_in (Al,A) ex v being Element of Valuations_in (Al,A) st
( ( for x being bound_QC-variable of Al st x <> Y holds
v . x = V1 . x ) & v . Y = V2 . Z ) by Lm3;