let x, y be Element of REAL ; :: thesis: ( + ((* (x,x)),(* (y,y))) = 0 implies x = 0 )
assume A1: + ((* (x,x)),(* (y,y))) = 0 ; :: thesis: x = 0
( * (x,x) in REAL+ & * (y,y) in REAL+ ) by Th16;
then consider x9, y9 being Element of REAL+ such that
A2: * (x,x) = x9 and
* (y,y) = y9 and
A3: 0 = x9 + y9 by A1, Def1;
A4: x9 = 0 by A3, ARYTM_2:5;
A5: x in REAL+ \/ [:{{}},REAL+:] by XBOOLE_0:def 5;

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

suppose x in REAL+ ; :: thesis: x = 0

then ex x9, y9 being Element of REAL+ st
( x = x9 & x = y9 & 0 = x9 *' y9 ) by A2, A4, Def2;
hence x = 0 by ARYTM_1:2; :: thesis: verum

end;

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

then consider x9, y9 being Element of REAL+ such that
A6: x = [0,x9] and
A7: x = [0,y9] and
A8: 0 = y9 *' x9 by A2, A4, Def2;
x9 = y9 by A6, A7, XTUPLE_0:1;
then x9 = 0 by A8, ARYTM_1:2;
then x in {[0,0]} by A6, TARSKI:def 1;
hence x = 0 by XBOOLE_0:def 5; :: thesis: verum

end;

end;