let f1, f2 be T-Sequence; :: thesis: rng (f1 ^ f2) = (rng f1) \/ (rng f2)
set f = f1 ^ f2;
set A1 = rng f1;
set A2 = rng f2;
X: dom (f1 ^ f2) = (dom f1) +^ (dom f2) by ORDINAL4:def 1;
thus rng (f1 ^ f2) c= (rng f1) \/ (rng f2) :: according to XBOOLE_0:def 10 :: thesis: (rng f1) \/ (rng f2) c= rng (f1 ^ f2)

proof

let y be set ; :: according to TARSKI:def 3 :: thesis: ( not y in rng (f1 ^ f2) or y in (rng f1) \/ (rng f2) )
assume y in rng (f1 ^ f2) ; :: thesis: y in (rng f1) \/ (rng f2)
then consider x being set such that
A5: x in dom (f1 ^ f2) and
A6: y = (f1 ^ f2) . x by FUNCT_1:def 3;
reconsider x = x as Ordinal by A5;

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

suppose A8: x in dom f1 ; :: thesis: y in (rng f1) \/ (rng f2)

then A9: f1 . x in rng f1 by FUNCT_1:def 3;
y = f1 . x by A6, A8, ORDINAL4:def 1;
hence y in (rng f1) \/ (rng f2) by A9, XBOOLE_0:def 3; :: thesis: verum

end;

suppose not x in dom f1 ; :: thesis: y in (rng f1) \/ (rng f2)

then dom f1 c= x by ORDINAL1:16;
then A10: (dom f1) +^ (x -^ (dom f1)) = x by ORDINAL3:def 5;
then A11: x -^ (dom f1) in dom f2 by X, A5, ORDINAL3:22;
then y = f2 . (x -^ (dom f1)) by A6, A10, ORDINAL4:def 1;
then y in rng f2 by A11, FUNCT_1:def 3;
hence y in (rng f1) \/ (rng f2) by XBOOLE_0:def 3; :: thesis: verum

end;

end;

end;

let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in (rng f1) \/ (rng f2) or x in rng (f1 ^ f2) )
assume A0: x in (rng f1) \/ (rng f2) ; :: thesis: x in rng (f1 ^ f2)
A1: dom f1 c= (dom f1) +^ (dom f2) by ORDINAL3:24;

per cases ( x in rng f1 or x in rng f2 ) by A0, XBOOLE_0:def 3;

suppose x in rng f1 ; :: thesis: x in rng (f1 ^ f2)

then consider z being set such that
A2: ( z in dom f1 & x = f1 . z ) by FUNCT_1:def 3;
x = (f1 ^ f2) . z by A2, ORDINAL4:def 1;
hence x in rng (f1 ^ f2) by X, A1, A2, FUNCT_1:def 3; :: thesis: verum

end;

suppose x in rng f2 ; :: thesis: x in rng (f1 ^ f2)

then consider z being set such that
A2: ( z in dom f2 & x = f2 . z ) by FUNCT_1:def 3;
reconsider z = z as Ordinal by A2;
A3: (dom f1) +^ z in dom (f1 ^ f2) by X, A2, ORDINAL3:17;
x = (f1 ^ f2) . ((dom f1) +^ z) by A2, ORDINAL4:def 1;
hence x in rng (f1 ^ f2) by A3, FUNCT_1:def 3; :: thesis: verum

end;

end;