let f, g be Sequence; :: thesis: rng (f ^ g) = (rng f) \/ (rng g)
A1: dom (f ^ g) = (dom f) +^ (dom g) by ORDINAL4:def 1;
thus rng (f ^ g) c= (rng f) \/ (rng g) :: according to XBOOLE_0:def 10 :: thesis: (rng f) \/ (rng g) c= rng (f ^ g)

proof

let y be object ; :: according to TARSKI:def 3 :: thesis: ( not y in rng (f ^ g) or y in (rng f) \/ (rng g) )
assume y in rng (f ^ g) ; :: thesis: y in (rng f) \/ (rng g)
then consider x being object such that
A2: ( x in dom (f ^ g) & y = (f ^ g) . x ) by FUNCT_1:def 3;

per cases ( x in dom f or ex a being Ordinal st
( a in dom g & x = (dom f) +^ a ) ) by A1, A2, ORDINAL3:38;

suppose A3: x in dom f ; :: thesis: y in (rng f) \/ (rng g)

then y = f . x by A2, ORDINAL4:def 1;
then y in rng f by A3, FUNCT_1:def 3;
hence y in (rng f) \/ (rng g) by XBOOLE_0:def 3; :: thesis: verum

end;

suppose ex a being Ordinal st
( a in dom g & x = (dom f) +^ a ) ; :: thesis: y in (rng f) \/ (rng g)

then consider a being Ordinal such that
A4: ( a in dom g & x = (dom f) +^ a ) ;
y = g . a by A2, A4, ORDINAL4:def 1;
then y in rng g by A4, FUNCT_1:def 3;
hence y in (rng f) \/ (rng g) by XBOOLE_0:def 3; :: thesis: verum

end;

end;

end;

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in (rng f) \/ (rng g) or x in rng (f ^ g) )
assume A5: x in (rng f) \/ (rng g) ; :: thesis: x in rng (f ^ g)

per cases ( x in rng f or x in rng g ) by A5, XBOOLE_0:def 3;

suppose x in rng f ; :: thesis: x in rng (f ^ g)

then consider y being object such that
A6: ( y in dom f & x = f . y ) by FUNCT_1:def 3;
( x = (f ^ g) . y & y in dom (f ^ g) ) by A1, A6, ORDINAL4:def 1, ORDINAL3:25;
hence x in rng (f ^ g) by FUNCT_1:def 3; :: thesis: verum

end;

suppose x in rng g ; :: thesis: x in rng (f ^ g)

then consider y being object such that
A7: ( y in dom g & x = g . y ) by FUNCT_1:def 3;
reconsider y = y as Ordinal by A7;
( x = (f ^ g) . ((dom f) +^ y) & (dom f) +^ y in dom (f ^ g) ) by A1, A7, ORDINAL4:def 1, ORDINAL3:17;
hence x in rng (f ^ g) by FUNCT_1:def 3; :: thesis: verum

end;

end;