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:
set F = f1 union f2;
assume A1: ( X1 misses X2 or f1 | (X1 meet X2) = f2 | (X1 meet X2) ) ; :: thesis:
thus rng (f1 union f2) c= (rng f1) \/ (rng f2) :: thesis:

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

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

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

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

end;

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

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

end;

end;

end;