theorem Th4: :: TOPREAL8:4

for f being FinSequence
for x being set holds
( x in rng f or x .. f = 0 )