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 x', y' being Element of REAL+ such that
A2: ( * x,x = x' & * y,y = y' ) and
A3: 0 = x' + y' by A1, Def2;
A4: x' = 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 x', y' being Element of REAL+ st
( x = x' & x = y' & 0 = x' *' y' ) by A2, A4, Def3;
hence x = 0 by ARYTM_1:2; :: thesis: verum

end;

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

then consider x', y' being Element of REAL+ such that
A6: ( x = [0 ,x'] & x = [0 ,y'] ) and
A7: 0 = y' *' x' by A2, A4, Def3;
x' = y' by A6, ZFMISC_1:33;
then x' = 0 by A7, 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;