let n be Nat; :: thesis: for x being Element of REAL n holds
( |(x,x)| = 0 iff x = 0* n )
let x be Element of REAL n; :: thesis: ( |(x,x)| = 0 iff x = 0* n )
thus ( |(x,x)| = 0 implies x = 0* n ) :: thesis: ( x = 0* n implies |(x,x)| = 0 )
proof
assume |(x,x)| = 0 ; :: thesis: x = 0* n
then |.x.| = 0 by Th16;
hence x = 0* n by EUCLID:8; :: thesis: verum
end;
thus ( x = 0* n implies |(x,x)| = 0 ) :: thesis: verum
proof
assume x = 0* n ; :: thesis: |(x,x)| = 0
then |(x,x)| = (1 / 4) * ((|.((0* n) + (0* n)).| ^2) - (|.((0* n) - (0* n)).| ^2)) by EUCLID_2:3
.= (1 / 4) * ((|.(0* n).| ^2) - (|.((0* n) - (0* n)).| ^2)) by Th1
.= (1 / 4) * 0 by RVSUM_1:32 ;
hence |(x,x)| = 0 ; :: thesis: verum
end;