set f = fi ^ psi;

consider A1 being Ordinal such that

A1: rng fi c= A1 by ORDINAL2:def 4;

consider A2 being Ordinal such that

A2: rng psi c= A2 by ORDINAL2:def 4;

A3: A2 c= A1 +^ A2 by ORDINAL3:24;

A1 c= A1 +^ A2 by ORDINAL3:24;

then A4: A1 \/ A2 c= A1 +^ A2 by A3, XBOOLE_1:8;

A5: 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 A5;

then rng (fi ^ psi) c= A1 +^ A2 by A4;

hence fi ^ psi is Ordinal-yielding ; :: thesis: verum

consider A1 being Ordinal such that

A1: rng fi c= A1 by ORDINAL2:def 4;

consider A2 being Ordinal such that

A2: rng psi c= A2 by ORDINAL2:def 4;

A3: A2 c= A1 +^ A2 by ORDINAL3:24;

A1 c= A1 +^ A2 by ORDINAL3:24;

then A4: A1 \/ A2 c= A1 +^ A2 by A3, XBOOLE_1:8;

A5: 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 A5;

then rng (fi ^ psi) c= A1 +^ A2 by A4;

hence fi ^ psi is Ordinal-yielding ; :: thesis: verum