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

A1: ( |(x,x)| = 0 ^2 implies |.x.| = 0 )

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

A1: ( |(x,x)| = 0 ^2 implies |.x.| = 0 )

proof

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

then x = 0* (len x) by Th6;

hence |.x.| = 0 by EUCLID:7; :: thesis: verum

end;then x = 0* (len x) by Th6;

hence |.x.| = 0 by EUCLID:7; :: thesis: verum

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