theorem :: EUCLID_2:8

for x being real-valued FinSequence holds
( |(x,x)| = 0 iff |.x.| = 0 )