set f = fi ^ psi;
consider A1 being Ordinal such that
A1: rng fi c= A1 by ORDINAL2:def 8;
consider A2 being Ordinal such that
A2: rng psi c= A2 by ORDINAL2:def 8;
A3: dom (fi ^ psi) = (dom fi) +^ (dom psi) by Def1;
A4: A2 c= A1 +^ A2 by ORDINAL3:27;
A7: A1 c= A1 +^ A2 by ORDINAL3:27;
then X1: A1 \/ A2 c= A1 +^ A2 by A4, XBOOLE_1:8;
X2: rng (fi ^ psi) c= (rng fi) \/ (rng psi) by Th2;
(rng fi) \/ (rng psi) c= A1 \/ A2 by A1, A2, XBOOLE_1:13;
then rng (fi ^ psi) c= A1 \/ A2 by X2, XBOOLE_1:1;
then rng (fi ^ psi) c= A1 +^ A2 by X1, XBOOLE_1:1;
hence fi ^ psi is Ordinal-yielding by ORDINAL2:def 8; :: thesis: verum