:: by Yatsuka Nakamura and Agata Darmochwa{\l}

::

:: Received November 21, 1991

:: Copyright (c) 1991-2021 Association of Mizar Users

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

g . x1 <> f . x2 ) holds

f +* g is one-to-one

proof end;

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

(rng f) \ (rng g) c= rng (f +* g)

proof end;

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)

(rng f) \/ (rng g) = rng (f +* g)

proof end;

reconsider dwa = 2 as Real ;

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} & f is being_homeomorphism & f . 1 = p & g is being_homeomorphism & g . 0 = p holds

ex h being Function of I[01],(T | (P \/ Q)) st

( h is being_homeomorphism & h . 0 = f . 0 & h . 1 = g . 1 )

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} & f is being_homeomorphism & f . 1 = p & g is being_homeomorphism & g . 0 = p holds

ex h being Function of I[01],(T | (P \/ Q)) st

( h is being_homeomorphism & h . 0 = f . 0 & h . 1 = g . 1 )

proof end;