let x, y be Surreal; :: thesis: ( x * (- y) = - (x * y) & (- x) * y = - (x * y) & (- x) * (- y) = x * y )
(- x) * (- y) = - ((- x) * y) by Lm8;
then (- x) * (- y) = - (- (x * y)) by Lm8;
hence ( x * (- y) = - (x * y) & (- x) * y = - (x * y) & (- x) * (- y) = x * y ) by Lm8; :: thesis: verum