theorem Th1: :: URYSOHN2:1
for A being Subset of REAL
for x being Real st x <> 0 holds
(x ") ** (x ** A) = A