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 x9 = x, y9 = 0 as Element of REAL+ by ARYTM_2:20;
0 = x9 *' y9 by ARYTM_2:4;
hence * (x,o) = 0 by A1, Def2; :: thesis: verum

end;

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

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

end;

end;