let x be real-valued FinSequence; :: thesis: ( |(x,x)| = 0 iff |.x.| = 0 )
A1: ( |(x,x)| = 0 ^2 implies |.x.| = 0 )

proof

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

end;

( |.x.| = 0 implies |(x,x)| = 0 ^2 ) by Th4;
hence ( |(x,x)| = 0 iff |.x.| = 0 ) by A1; :: thesis: verum