let fi, psi be Sequence; :: thesis: rng (fi ^ psi) c= (rng fi) \/ (rng psi)
set f = fi ^ psi;
set A1 = rng fi;
set A2 = rng psi;
A1: dom (fi ^ psi) = (dom fi) +^ (dom psi) by Def1;
let y be object ; :: 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 object such that
A2: x in dom (fi ^ psi) and
A3: y = (fi ^ psi) . x by FUNCT_1:def 3;
reconsider x = x as Ordinal by A2;
per cases ( x in dom fi or not x in dom fi ) ;
suppose A4: x in dom fi ; :: thesis: y in (rng fi) \/ (rng psi)
then A5: fi . x in rng fi by FUNCT_1:def 3;
y = fi . x by A3, A4, Def1;
then y in rng fi by A5;
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:16;
then A6: (dom fi) +^ (x -^ (dom fi)) = x by ORDINAL3:def 5;
then A7: x -^ (dom fi) in dom psi by A1, A2, ORDINAL3:22;
then y = psi . (x -^ (dom fi)) by A3, A6, Def1;
then y in rng psi by A7, FUNCT_1:def 3;
then y in rng psi ;
hence y in (rng fi) \/ (rng psi) by XBOOLE_0:def 3; :: thesis: verum
end;
end;