let X, Y be non empty TopSpace; :: thesis:
let X1, X2 be non empty SubSpace of X; :: thesis:
let f1 be Function of X1,Y; :: thesis:
let f2 be Function of X2,Y; :: thesis:
assume A1: ( X1 misses X2 or f1 | (X1 meet X2) = f2 | (X1 meet X2) ) ; :: thesis:
set F = f1 union f2;
thus rng (f1 union f2) c= (rng f1) \/ (rng f2) :: thesis:

let y be set ; :: according to TARSKI:def 3 :: thesis:
assume y in rng (f1 union f2) ; :: thesis:
then consider x being set such that
A2: x in dom (f1 union f2) and
A3: (f1 union f2) . x = y by FUNCT_1:def 5;
A4: ( the carrier of X1 = dom f1 & the carrier of X2 = dom f2 ) by FUNCT_2:def 1;
A5: the carrier of (X1 union X2) = the carrier of X1 \/ the carrier of X2 by TSEP_1:def 2;
A6: x is Point of X by A2, PRE_TOPC:55;

per cases by A2, A5, XBOOLE_0:def 3;

suppose A7: x in the carrier of X1 ; :: thesis:

then A8: f1 . x in rng f1 by A4, FUNCT_1:def 5;
(f1 union f2) . x = f1 . x by A1, A6, A7, Th14;
hence y in (rng f1) \/ (rng f2) by A3, A8, XBOOLE_0:def 3; :: thesis:

end;

suppose A9: x in the carrier of X2 ; :: thesis:

then A10: f2 . x in rng f2 by A4, FUNCT_1:def 5;
(f1 union f2) . x = f2 . x by A1, A6, A9, Th14;
hence y in (rng f1) \/ (rng f2) by A3, A10, XBOOLE_0:def 3; :: thesis:

end;