let x, y be Element of REAL ; ( + ((* (x,x)),(* (y,y))) = 0 implies x = 0 )
assume A1:
+ ((* (x,x)),(* (y,y))) = 0
; 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 [:{0},REAL+:]
;
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;
verum end; end;