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 )

( |(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

thus
( x = 0* n implies |(x,x)| = 0 )
:: thesis: verum
assume
|(x,x)| = 0
; :: thesis: x = 0* n

then |.x.| = 0 by Th16;

hence x = 0* n by EUCLID:8; :: thesis: verum

end;then |.x.| = 0 by Th16;

hence x = 0* n by EUCLID:8; :: thesis: verum