let n be Nat; :: thesis: for x being Element of REAL n holds

( |(x,x)| = 0 iff |.x.| = 0 )

let x be Element of REAL n; :: thesis: ( |(x,x)| = 0 iff |.x.| = 0 )

thus ( |(x,x)| = 0 implies |.x.| = 0 ) :: thesis: ( |.x.| = 0 implies |(x,x)| = 0 )

hence ( |.x.| = 0 implies |(x,x)| = 0 ) ; :: thesis: verum

( |(x,x)| = 0 iff |.x.| = 0 )

let x be Element of REAL n; :: thesis: ( |(x,x)| = 0 iff |.x.| = 0 )

thus ( |(x,x)| = 0 implies |.x.| = 0 ) :: thesis: ( |.x.| = 0 implies |(x,x)| = 0 )

proof

( |.x.| = 0 implies |(x,x)| = 0 ^2 )
by EUCLID_2:4;
assume
|(x,x)| = 0
; :: thesis: |.x.| = 0

then |.x.| ^2 = 0 by EUCLID_2:4;

hence |.x.| = 0 by XCMPLX_1:6; :: thesis: verum

end;then |.x.| ^2 = 0 by EUCLID_2:4;

hence |.x.| = 0 by XCMPLX_1:6; :: thesis: verum

hence ( |.x.| = 0 implies |(x,x)| = 0 ) ; :: thesis: verum