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, Def5;
thus y = * j,y by Th21
.= * (* x,y),(inv x) by A3, Th15
.= 0 by A1, Th14 ; :: thesis: verum