theorem :: SURREALR:54

for x1, x2, y being Surreal st x1 == x2 holds
x1 * y == x2 * y by Th51;