set f = fi ^ psi;
A1: dom (fi ^ psi) = (dom fi) +^ (dom psi) by Def1;
consider A1 being Ordinal such that
A2: rng fi c= A1 by ORDINAL2:def 8;
consider A2 being Ordinal such that
A3: rng psi c= A2 by ORDINAL2:def 8;
rng (fi ^ psi) c= A1 +^ A2

proof

let y be set ; :: according to TARSKI:def 3 :: thesis: ( not y in rng (fi ^ psi) or y in A1 +^ A2 )
assume y in rng (fi ^ psi) ; :: thesis: y in A1 +^ A2
then consider x being set such that
A4: ( x in dom (fi ^ psi) & y = (fi ^ psi) . x ) by FUNCT_1:def 5;
reconsider x = x as Ordinal by A4;
A5: ( A1 c= A1 +^ A2 & A2 c= A1 +^ A2 ) by ORDINAL3:27;

now

per cases ( x in dom fi or not x in dom fi ) ;

suppose x in dom fi ; :: thesis: y in A1 +^ A2

then ( y = fi . x & fi . x in rng fi ) by A4, Def1, FUNCT_1:def 5;
then y in A1 by A2;
hence y in A1 +^ A2 by A5; :: thesis: verum

end;

suppose not x in dom fi ; :: thesis: y in A1 +^ A2

then dom fi c= x by ORDINAL1:26;
then A6: (dom fi) +^ (x -^ (dom fi)) = x by ORDINAL3:def 6;
then A7: x -^ (dom fi) in dom psi by A1, A4, ORDINAL3:25;
then y = psi . (x -^ (dom fi)) by A4, A6, Def1;
then y in rng psi by A7, FUNCT_1:def 5;
then y in A2 by A3;
hence y in A1 +^ A2 by A5; :: thesis: verum

end;

end;

end;

hence y in A1 +^ A2 ; :: thesis: verum

end;

hence fi ^ psi is Ordinal-yielding by ORDINAL2:def 8; :: thesis: verum