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 x', y' being Element of REAL+ st
( x = x' & x = y' & * x,x = x' *' y' ) by Def3;
hence * x,x in REAL+ ; :: thesis: verum

end;

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

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

end;

end;