reconsider f = 0 --> omega as Ordinal-Sequence ;
take f ; :: thesis: f is finite
thus f is finite ; :: thesis: verum