let x, y be Element of REAL ; ( ( y <> 0 implies * (y,x) = 1 ) & ( not y <> 0 implies x = 0 ) implies ( ( x <> 0 implies * (x,y) = 1 ) & ( not x <> 0 implies y = 0 ) ) )
assume that
A76:
( y <> 0 implies * (y,x) = 1 )
and
A77:
( y = 0 implies x = 0 )
; ( ( x <> 0 implies * (x,y) = 1 ) & ( not x <> 0 implies y = 0 ) )
thus
( x <> 0 implies * (x,y) = 1 )
by A76, A77; ( not x <> 0 implies y = 0 )
assume A78:
x = 0
; y = 0
A79:
y in REAL+ \/ [:{0},REAL+:]
by XBOOLE_0:def 5;
assume A80:
y <> 0
; contradiction
per cases
( y in REAL+ or y in [:{0},REAL+:] )
by A79, XBOOLE_0:def 3;
suppose A81:
y in [:{0},REAL+:]
;
contradictionA82:
not
x in [:{0},REAL+:]
by A78, Th5, ARYTM_2:20, XBOOLE_0:3;
not
y in REAL+
by A81, Th5, XBOOLE_0:3;
hence
contradiction
by A76, A78, A80, A82, Def2;
verum end;