let x be Element of REAL ; :: thesis: * x,x in REAL+
A1: x in REAL+ \/ [:{{} },REAL+ :] by NUMBERS:def 1, XBOOLE_0:def 5;

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

suppose x in REAL+ ; :: thesis: * x,x in REAL+

then ex x9, y9 being Element of REAL+ st
( x = x9 & x = y9 & * x,x = x9 *' y9 ) by Def3;
hence * x,x in REAL+ ; :: thesis: verum

end;

suppose x in [:{0 },REAL+ :] ; :: thesis: * x,x in REAL+

then ex x9, y9 being Element of REAL+ st
( x = [0 ,x9] & x = [0 ,y9] & * x,x = y9 *' x9 ) by Def3;
hence * x,x in REAL+ ; :: thesis: verum

end;

end;