let x, y be Element of REAL ; :: thesis: ( ( 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 ) ; :: thesis: ( ( x <> 0 implies * (x,y) = 1 ) & ( not x <> 0 implies y = 0 ) )
thus ( x <> 0 implies * (x,y) = 1 ) by A76, A77; :: thesis: ( not x <> 0 implies y = 0 )
assume A78: x = 0 ; :: thesis: y = 0
A79: y in REAL+ \/ [:{0},REAL+:] by XBOOLE_0:def 5;
assume A80: y <> 0 ; :: thesis: contradiction

per cases ( y in REAL+ or y in [:{0},REAL+:] ) by A79, XBOOLE_0:def 3;

suppose y in REAL+ ; :: thesis: contradiction

then ex x9, y9 being Element of REAL+ st
( x = x9 & y = y9 & 1 = x9 *' y9 ) by A76, A78, A80, Def2, ARYTM_2:20;
hence contradiction by A78, ARYTM_2:4; :: thesis: verum

end;

suppose A81: y in [:{0},REAL+:] ; :: thesis: contradiction

A82: 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; :: thesis: verum

end;

end;