let x be FinSequence of REAL ; :: 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 )

proof

assume |(x,x)| = 0 ; :: thesis: x = 0* (len x)
then |.x.| ^2 = 0 by Th12;
then A1: |.x.| = 0 by XCMPLX_1:6;
reconsider y = x as Element of REAL (len x) by JORDAN2C:52;
y = 0* (len x) by A1, EUCLID:11;
hence x = 0* (len x) ; :: thesis: verum

end;

assume x = 0* (len x) ; :: thesis: |(x,x)| = 0
then |.x.| = 0 by EUCLID:10;
then |(x,x)| = 0 ^2 by Th12;
hence |(x,x)| = 0 ; :: thesis: verum