A1: rng (X --> o) c= {o} by FUNCOP_1:19;
{o} c= succ o by XBOOLE_1:7;
then rng (X --> o) c= succ o by A1, XBOOLE_1:1;
hence X --> o is Ordinal-yielding by Def8; :: thesis: verum