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;