theorem :: SURREALI:45
for x, y being Surreal st not x == 0_No & not y == 0_No holds
(x * y) " == (x ") * (y ")