let x be Element of REAL ; :: thesis: * (x,x) in REAL+
A1: x in REAL+ \/ [:{{}},REAL+:] by 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 Def2;
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 Def2;
hence * (x,x) in REAL+ ; :: thesis: verum

end;

end;