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;

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 )
;

end;

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

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