let x, y be ExtReal; :: thesis: ( not x is real & x * y = 0 implies y = 0 )
assume that
A1: not x is real and
A2: x * y = 0 ; :: thesis: y = 0
( not ( x is positive & y is positive ) & not ( x is negative & y is negative ) ) by A2;
hence y = 0 by A1, A2; :: thesis: verum