:: Some Facts about Union of Two Functions and Continuity of Union of Functions
:: by Yatsuka Nakamura and Agata Darmochwa{\l}
::
:: Received November 21, 1991
:: Copyright (c) 1991-2012 Association of Mizar Users


begin

theorem :: TOPMETR2:1
for f, g being Function st f is one-to-one & g is one-to-one & ( for x1, x2 being set st x1 in dom g & x2 in (dom f) \ (dom g) holds
g . x1 <> f . x2 ) holds
f +* g is one-to-one
proofend;

Lm1:  for f, g being Function st f .: ((dom f) /\ (dom g)) c= rng g holds
(rng f) \ (rng g) c= rng (f +* g)
proofend;

theorem :: TOPMETR2:2
for f, g being Function st f .: ((dom f) /\ (dom g)) c= rng g holds
(rng f) \/ (rng g) = rng (f +* g)
proofend;

theorem :: TOPMETR2:3
for T being T_2 TopSpace
for P, Q being Subset of T
for p being Point of T
for f being Function of I[01],(T | P)
for g being Function of I[01],(T | Q) st P /\ Q = {p} &amp; f is being_homeomorphism &amp; f . 1 = p &amp; g is being_homeomorphism &amp; g . 0 = p holds
ex h being Function of I[01],(T | (P \/ Q)) st
( h is being_homeomorphism &amp; h . 0 = f . 0 &amp; h . 1 = g . 1 )
proofend;