consider a being Ordinal such that
A1: rng A c= a by ORDINAL2:def 4;
rng (A /^ n) c= rng A by Th9;
hence A /^ n is Ordinal-yielding by A1, XBOOLE_1:1, ORDINAL2:def 4; :: thesis: verum