theorem Th2: :: TOPREAL8:2

for f being non trivial FinSequence holds 1 < len f