theorem Th8: :: EUCLID_2:9

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