let fi, psi be Ordinal-Sequence; :: thesis: rng (fi ^ psi) c= (rng fi) \/ (rng psi)
set f = fi ^ psi;
set A1 = rng fi;
set A2 = rng psi;
X: dom (fi ^ psi) = (dom fi) +^ (dom psi) by Def1;
let y be set ; :: according to TARSKI:def 3 :: thesis: ( not y in rng (fi ^ psi) or y in (rng fi) \/ (rng psi) )
assume y in rng (fi ^ psi) ; :: thesis: y in (rng fi) \/ (rng psi)
then consider x being set such that
A5: x in dom (fi ^ psi) and
A6: y = (fi ^ psi) . x by FUNCT_1:def 5;
reconsider x = x as Ordinal by A5;

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

suppose A8: x in dom fi ; :: thesis: y in (rng fi) \/ (rng psi)

then A9: fi . x in rng fi by FUNCT_1:def 5;
y = fi . x by A6, A8, Def1;
then y in rng fi by A9;
hence y in (rng fi) \/ (rng psi) by XBOOLE_0:def 3; :: thesis: verum

end;

suppose not x in dom fi ; :: thesis: y in (rng fi) \/ (rng psi)

then dom fi c= x by ORDINAL1:26;
then A10: (dom fi) +^ (x -^ (dom fi)) = x by ORDINAL3:def 6;
then A11: x -^ (dom fi) in dom psi by X, A5, ORDINAL3:25;
then y = psi . (x -^ (dom fi)) by A6, A10, Def1;
then y in rng psi by A11, FUNCT_1:def 5;
then y in rng psi ;
hence y in (rng fi) \/ (rng psi) by XBOOLE_0:def 3; :: thesis: verum

end;

end;