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

proof

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: ( not y in rng (f1 union f2) or y in (rng f1) \/ (rng f2) )
A4: the carrier of X1 = dom f1 by FUNCT_2:def 1;
assume y in rng (f1 union f2) ; :: thesis: y in (rng f1) \/ (rng f2)
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 ( x in the carrier of X1 or x in the carrier of X2 ) by A5, A2, XBOOLE_0:def 3;

suppose x in the carrier of X1 ; :: thesis: y in (rng f1) \/ (rng f2)

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: verum

end;

suppose x in the carrier of X2 ; :: thesis: y in (rng f1) \/ (rng f2)

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: verum

end;

end;

end;