theorem :: SURREALR:77
for x, y being Surreal holds
( x * y == 0_No iff ( x == 0_No or y == 0_No ) ) by Th72, Th74;