:: 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-2021 Association of Mizar Users
::           (Stowarzyszenie Uzytkownikow Mizara, Bialystok, Poland).
:: This code can be distributed under the GNU General Public Licence
:: version 3.0 or later, or the Creative Commons Attribution-ShareAlike
:: License version 3.0 or later, subject to the binding interpretation
:: detailed in file COPYING.interpretation.
:: See COPYING.GPL and COPYING.CC-BY-SA for the full text of these
:: licenses, or see http://www.gnu.org/licenses/gpl.html and
:: http://creativecommons.org/licenses/by-sa/3.0/.

environ

 vocabularies NUMBERS, REAL_1, FUNCT_1, RELAT_1, XBOOLE_0, FUNCT_4, TARSKI,
      PRE_TOPC, SUBSET_1, BORSUK_1, TOPS_2, CARD_1, ARYTM_3, XXREAL_0,
      XXREAL_1, TOPMETR, STRUCT_0, ORDINAL2, RCOMP_1, ARYTM_1, PCOMPS_1,
      METRIC_1, FUNCT_7;
 notations TARSKI, XBOOLE_0, SUBSET_1, ORDINAL1, NUMBERS, XCMPLX_0, XREAL_0,
      REAL_1, RELAT_1, FUNCT_1, RELSET_1, PARTFUN1, FUNCT_2, FUNCT_4, STRUCT_0,
      PRE_TOPC, TOPS_2, COMPTS_1, RCOMP_1, METRIC_1, PCOMPS_1, TOPMETR,
      XXREAL_0;
 constructors FUNCT_4, REAL_1, MEMBERED, RCOMP_1, TOPS_2, COMPTS_1, TOPMETR,
      XXREAL_2, PCOMPS_1;
 registrations XBOOLE_0, RELSET_1, FUNCT_2, NUMBERS, MEMBERED, STRUCT_0,
      PRE_TOPC, METRIC_1, PCOMPS_1, BORSUK_1, TOPMETR, XXREAL_2, XREAL_0;
 requirements REAL, NUMERALS, SUBSET, BOOLE, ARITHM;


begin

reserve x,r,a for Real;
reserve f,g for Function,
  x1,x2 for set;

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

theorem :: TOPMETR2:2
  f.:(dom f /\ dom g) c= rng g implies rng f \/ rng g = rng(f+*g);

reserve T for T_2 TopSpace;

theorem :: TOPMETR2:3
  for P, Q being Subset of T for p being Point of T, f being Function of
  I[01], T|P, 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 ex h being
Function of I[01], T|(P \/ Q) st h is being_homeomorphism & h.0 = f.0 & h.1 = g
  .1;