reconsider jj = 1 as Element of REAL by NUMBERS:19;
let x, y be Element of REAL ; :: thesis: ( not * (x,y) = 0 or x = 0 or y = 0 )
assume that
A1: * (x,y) = 0 and
A2: x <> 0 ; :: thesis: y = 0
A3: * (x,(inv x)) = 1 by A2, Def4;
thus y = * (jj,y) by Th19
.= * ((* (x,y)),(inv x)) by A3, Th13
.= 0 by A1, Th12 ; :: thesis: verum