theorem Th1: :: PROB_3:1

for f being FinSequence holds not 0 in dom f