theorem :: EUCLID_2:10

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