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 Th18;
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, Def2;
A4: x9 = 0 by A3, ARYTM_2:6;
A5: x in REAL+ \/ [:{{} },REAL+ :] by NUMBERS:def 1, 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, Def3;
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, Def3;
x9 = y9 by A6, A7, ZFMISC_1:33;
then x9 = 0 by A8, ARYTM_1:2;
then x in {[0 ,0 ]} by A6, TARSKI:def 1;
hence x = 0 by NUMBERS:def 1, XBOOLE_0:def 5; :: thesis: verum

end;

end;