let x be real-valued FinSequence; :: thesis: ( |(x,x)| = 0 iff x = 0* (len x) )

thus ( |(x,x)| = 0 implies x = 0* (len x) ) :: thesis: ( x = 0* (len x) implies |(x,x)| = 0 )

then |.x.| = 0 by EUCLID:7;

then |(x,x)| = 0 ^2 by Th4;

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

thus ( |(x,x)| = 0 implies x = 0* (len x) ) :: thesis: ( x = 0* (len x) implies |(x,x)| = 0 )

proof

assume
x = 0* (len x)
; :: thesis: |(x,x)| = 0
x is FinSequence of REAL
by Lm1;

then reconsider y = x as Element of REAL (len x) by EUCLID:76;

assume |(x,x)| = 0 ; :: thesis: x = 0* (len x)

then |.x.| ^2 = 0 by Th4;

then |.x.| = 0 by XCMPLX_1:6;

then y = 0* (len x) by EUCLID:8;

hence x = 0* (len x) ; :: thesis: verum

end;then reconsider y = x as Element of REAL (len x) by EUCLID:76;

assume |(x,x)| = 0 ; :: thesis: x = 0* (len x)

then |.x.| ^2 = 0 by Th4;

then |.x.| = 0 by XCMPLX_1:6;

then y = 0* (len x) by EUCLID:8;

hence x = 0* (len x) ; :: thesis: verum

then |.x.| = 0 by EUCLID:7;

then |(x,x)| = 0 ^2 by Th4;

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