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