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