let x, o be Element of REAL ; :: thesis: ( o = 0 implies * x,o = 0 )
assume A1: o = 0 ; :: thesis: * x,o = 0

per cases ( x in REAL+ or not x in REAL+ ) ;

suppose x in REAL+ ; :: thesis: * x,o = 0

then reconsider x' = x, y' = 0 as Element of REAL+ by ARYTM_2:21;
0 = x' *' y' by ARYTM_2:4;
hence * x,o = 0 by A1, Def3; :: thesis: verum

end;

suppose A2: not x in REAL+ ; :: thesis: * x,o = 0

not o in [:{{} },REAL+ :] by A1, Th5, ARYTM_2:21, XBOOLE_0:3;
hence * x,o = 0 by A1, A2, Def3; :: thesis: verum

end;

end;