theorem Th6: :: EUCLID_2:7

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