:: 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-2016 Association of Mizar Users

environ

vocabularies HIDDEN, 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 HIDDEN, 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;
definitions TARSKI;
theorems BORSUK_1, COMPTS_1, FUNCT_1, FUNCT_2, FUNCT_4, HEINE, TOPMETR, PCOMPS_1, PRE_TOPC, RCOMP_1, TARSKI, TOPS_2, RELSET_1, XBOOLE_0, XBOOLE_1, XREAL_1, XXREAL_1, XXREAL_2, RELAT_1, XREAL_0;
schemes CLASSES1, FUNCT_2;
registrations XBOOLE_0, RELSET_1, FUNCT_2, NUMBERS, MEMBERED, STRUCT_0, PRE_TOPC, METRIC_1, PCOMPS_1, BORSUK_1, TOPMETR, XXREAL_2, XREAL_0;
constructors HIDDEN, FUNCT_4, REAL_1, MEMBERED, RCOMP_1, TOPS_2, COMPTS_1, TOPMETR, XXREAL_2, PCOMPS_1;
requirements HIDDEN, REAL, NUMERALS, SUBSET, BOOLE, ARITHM;
equalities STRUCT_0;
expansions TARSKI;


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
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)
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 )
proof end;