take f = I --> omega; :: thesis: f is infinite-yielding
let J be set ; :: according to MSAFREE5:def 8 :: thesis: ( J in rng f implies J is infinite )
assume A1: J in rng f ; :: thesis: J is infinite
rng f c= {omega} by FUNCOP_1:13;
hence J is infinite by A1, TARSKI:def 1; :: thesis: verum