theorem Th5: :: ORDINAL5:5

for f being Sequence holds
( f is infinite iff omega c= dom f )