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 NUMBERS:def 1, 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, Def3, ARYTM_2:21;
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:21, XBOOLE_0:3;
not y in REAL+ by A81, Th5, XBOOLE_0:3;
hence contradiction by A76, A78, A80, A82, Def3; :: thesis: verum

end;

end;