:: 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
::           (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;
 definitions TARSKI;
 equalities STRUCT_0;
 expansions 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;

begin

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

theorem
  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
proof
  assume that
A1: f is one-to-one and
A2: g is one-to-one and
A3: for x1,x2 st x1 in dom g & x2 in dom f \ dom g holds g.x1 <> f.x2;
  now
    let x11,x22 be object;
    assume that
A4: x11 in dom (f+*g) and
A5: x22 in dom (f+*g) and
A6: (f+*g).x11 = (f+*g).x22;
A7: x22 in dom f \/ dom g by A5,FUNCT_4:def 1;
    then
A8: x22 in (dom f \ dom g) \/ dom g by XBOOLE_1:39;
A9: x11 in dom f \/ dom g by A4,FUNCT_4:def 1;
    then
A10: x11 in (dom f \ dom g) \/ dom g by XBOOLE_1:39;
    now
      per cases by A10,XBOOLE_0:def 3;
      suppose
A11:    x11 in (dom f \ dom g);
        then not x11 in dom g by XBOOLE_0:def 5;
        then
A12:    (f+*g).x11 = f.x11 by A9,FUNCT_4:def 1;
        now
          per cases by A8,XBOOLE_0:def 3;
          case
A13:        x22 in (dom f \ dom g);
            then not x22 in dom g by XBOOLE_0:def 5;
            then f.x11 = f.x22 by A6,A7,A12,FUNCT_4:def 1;
            hence x11 = x22 by A1,A11,A13,FUNCT_1:def 4;
          end;
          case
A14:        x22 in dom g;
            then g.x22 <> f.x11 by A3,A11;
            hence contradiction by A6,A7,A12,A14,FUNCT_4:def 1;
          end;
        end;
        hence x11 = x22;
      end;
      suppose
A15:    x11 in dom g;
        now
          per cases by A8,XBOOLE_0:def 3;
          case
A16:        x22 in (dom f \ dom g);
            then not x22 in dom g by XBOOLE_0:def 5;
            then
A17:        (f+*g).x22 = f.x22 by A7,FUNCT_4:def 1;
            g.x11 <> f.x22 by A3,A15,A16;
            hence contradiction by A6,A9,A15,A17,FUNCT_4:def 1;
          end;
          case
A18:        x22 in dom g;
            then (f+*g).x22 = g.x22 by A7,FUNCT_4:def 1;
            then g.x11 = g.x22 by A6,A9,A15,FUNCT_4:def 1;
            hence x11 = x22 by A2,A15,A18,FUNCT_1:def 4;
          end;
        end;
        hence x11 = x22;
      end;
    end;
    hence x11 = x22;
  end;
  hence thesis by FUNCT_1:def 4;
end;

Lm1: f.:(dom f /\ dom g) c= rng g implies rng f \ rng g c= rng(f+*g)
proof
  assume
A1: f.:(dom f /\ dom g) c= rng g;
  let y1 be object;
  assume
A2: y1 in rng f \ rng g;
  then consider x1 being object such that
A3: x1 in dom f and
A4: y1 = f.x1 by FUNCT_1:def 3;
A5: x1 in dom f \/ dom g by A3,XBOOLE_0:def 3;
  then
A6: x1 in dom (f+*g) by FUNCT_4:def 1;
  now
    assume x1 in dom g;
    then x1 in dom f /\ dom g by A3,XBOOLE_0:def 4;
    then f.x1 in f.:(dom f /\ dom g) by A3,FUNCT_1:def 6;
    hence contradiction by A1,A2,A4,XBOOLE_0:def 5;
  end;
  then (f+*g).x1 = f.x1 by A5,FUNCT_4:def 1;
  hence thesis by A4,A6,FUNCT_1:def 3;
end;

theorem
  f.:(dom f /\ dom g) c= rng g implies rng f \/ rng g = rng(f+*g)
proof
  assume f.:(dom f /\ dom g) c= rng g;
  then
A1: rng f \ rng g c= rng(f+*g) by Lm1;
  rng g c= rng(f +* g) by FUNCT_4:18;
  then (rng f \ rng g) \/ rng g c= rng(f +* g) by A1,XBOOLE_1:8;
  then
A2: rng f \/ rng g c= rng(f +* g) by XBOOLE_1:39;
  rng(f+*g) c= rng f \/ rng g by FUNCT_4:17;
  hence thesis by A2,XBOOLE_0:def 10;
end;

reserve T for T_2 TopSpace;

    reconsider dwa=2 as Real;

theorem
  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
proof
  1/2 in { r where r is Real: 0 <= r & r <= 1};
  then reconsider pp = 1/2 as Point of I[01] by BORSUK_1:40,RCOMP_1:def 1;
  reconsider PP = [. 0,1/2 .] as Subset of R^1 by TOPMETR:17;
A1: 1/2 in [. 0,1 .] by XXREAL_1:1;
  1 in [. 0,1 .] by XXREAL_1:1;
  then [. 1/2,1 .] c= the carrier of I[01] by A1,BORSUK_1:40,XXREAL_2:def 12;
  then
A2: the carrier of (Closed-Interval-TSpace(1/2,1)) c= the carrier of I[01]
  by TOPMETR:18;
  0 in [. 0,1 .] by XXREAL_1:1;
  then [. 0,1/2 .] c= the carrier of I[01] by A1,BORSUK_1:40,XXREAL_2:def 12;
  then the carrier of (Closed-Interval-TSpace(0,1/2)) c= the carrier of I[01]
  by TOPMETR:18;
  then reconsider
  T1 = Closed-Interval-TSpace(0,1/2),T2 = Closed-Interval-TSpace(1/
  2,1) as SubSpace of I[01] by A2,TOPMETR:3;
  deffunc U(Real) = In(2*$1,REAL);
  let P, Q be Subset of T;
  let p be Point of T;
  let f be Function of I[01], T|P, g be Function of I[01], T|Q;
  assume that
A3: P /\ Q = {p} and
A4: f is being_homeomorphism and
A5: f.1 = p and
A6: g is being_homeomorphism and
A7: g.0 = p;
  Q = [#](T | Q) by PRE_TOPC:def 5;
  then
A8: rng g = Q by A6,TOPS_2:def 5;
  p in P /\ Q by A3,TARSKI:def 1;
  then reconsider M = T as non empty TopSpace;
  reconsider P9=P, Q9=Q as non empty Subset of M by A3;
  reconsider R = P9 \/ Q9 as non empty Subset of M;
A9: M|P9 is SubSpace of M|R by TOPMETR:4;
  defpred X[object,object] means for a st a=$1 holds $2 = f.(2*a);
  consider f3 being Function of REAL,REAL such that
A10: for x being Element of REAL holds f3.x = U(x) from FUNCT_2:sch 4;
A11: R = [#] (M|R) by PRE_TOPC:def 5
    .= the carrier of M|R;
  then dom g = the carrier of I[01] by FUNCT_2:def 1;
  then reconsider g9 = g as Function of I[01],M|R by A8,A11,RELSET_1:4
,XBOOLE_1:7;
A12: M|Q9 is SubSpace of M|R by TOPMETR:4;
  g is continuous by A6,TOPS_2:def 5;
  then
A13: g9 is continuous by A12,PRE_TOPC:26;
  reconsider PP as non empty Subset of R^1 by XXREAL_1:1;
A14: T1 is compact & T2 is compact by HEINE:4;
  P = [#](T | P) by PRE_TOPC:def 5;
  then
A15: rng f = P by A4,TOPS_2:def 5;
  dom f = the carrier of I[01] by A11,FUNCT_2:def 1;
  then reconsider ff=f as Function of I[01],M|R by A15,A11,RELSET_1:4
,XBOOLE_1:7;
  f is continuous by A4,TOPS_2:def 5;
  then
A16: ff is continuous by A9,PRE_TOPC:26;
  reconsider f3 as Function of R^1,R^1 by TOPMETR:17;
A17: dom (f3| [.0,1/2.]) = dom f3 /\ [. 0,1/2 .] by RELAT_1:61
    .= REAL /\ [. 0,1/2 .] by FUNCT_2:def 1
    .= [. 0,1/2 .] by XBOOLE_1:28
    .= the carrier of T1 by TOPMETR:18;
  rng (f3| [.0,1/2.]) c= the carrier of R^1;
  then reconsider f39 = f3|PP as Function of T1,R^1 by A17,FUNCT_2:def 1
,RELSET_1:4;
A18: dom f39 = the carrier of T1 by FUNCT_2:def 1;
  rng f39 c= the carrier of I[01]
  proof
    let y be object;
    assume y in rng f39;
    then consider x being object such that
A19: x in dom f39 and
A20: y = f39.x by FUNCT_1:def 3;
    x in [. 0,1/2 .] by A18,A19,TOPMETR:18;
    then x in {r where r is Real: 0 <= r & r <= 1/2} by RCOMP_1:def 1;
    then consider r being Real such that
A21: x = r and
A22: 0 <= r & r <= 1/2;
A23: 2*0 <= 2*r & 2*r <= 2*(1/2) by A22,XREAL_1:64;
    reconsider r as Element of REAL by XREAL_0:def 1;
    y = f3.x by A19,A20,FUNCT_1:47
      .= U(r) by A10,A21;
    then y in {rr where rr is Real: 0 <= rr & rr <= 1} by A23;
    hence thesis by BORSUK_1:40,RCOMP_1:def 1;
  end;
  then reconsider f4 = f39 as Function of T1,I[01] by A18,RELSET_1:4;
A24: R^1|PP = T1 by TOPMETR:19;
  f3.x = dwa*x + 0
  proof
   reconsider x as Element of REAL by XREAL_0:def 1;
    f3.x = U(x) + 0 by A10;
   hence thesis;
  end;
  then f39 is continuous by A24,TOPMETR:7,21;
  then
A25: f4 is continuous by PRE_TOPC:27;
  reconsider PP = [. 1/2,1 .] as Subset of R^1 by TOPMETR:17;
  reconsider PP as non empty Subset of R^1 by XXREAL_1:1;
  deffunc U1(Real) = In(2*$1-1,REAL);
  consider g3 being Function of REAL,REAL such that
A26: for x being Element of REAL holds g3.x = U1(x) from FUNCT_2:sch 4;
  reconsider g3 as Function of R^1,R^1 by TOPMETR:17;
A27: dom (g3| [. 1/2,1 .]) = dom g3 /\ [. 1/2,1 .] by RELAT_1:61
    .= REAL /\ [. 1/2,1 .] by FUNCT_2:def 1
    .= [. 1/2,1 .] by XBOOLE_1:28
    .= the carrier of T2 by TOPMETR:18;
  rng (g3| [. 1/2,1 .]) c= the carrier of R^1;
  then reconsider g39 = g3|PP as Function of T2,R^1 by A27,FUNCT_2:def 1
,RELSET_1:4;
A28: dom g39 = the carrier of T2 by FUNCT_2:def 1;
  rng g39 c= the carrier of I[01]
  proof
    let y be object;
    assume y in rng g39;
    then consider x being object such that
A29: x in dom g39 and
A30: y = g39.x by FUNCT_1:def 3;
    x in [. 1/2,1 .] by A28,A29,TOPMETR:18;
    then x in {r where r is Real: 1/2 <= r & r <= 1} by RCOMP_1:def 1;
    then consider r being Real such that
A31: x = r and
A32: 1/2 <= r and
A33: r <= 1;
    2*(1/2) <= 2*r by A32,XREAL_1:64;
    then
A34: 1 - 1 <= 2*r - 1 by XREAL_1:9;
    2*r <= 2*1 by A33,XREAL_1:64;
    then
A35: 2*r - 1 <= (1 + 1) - 1 by XREAL_1:9;
    reconsider r as Element of REAL by XREAL_0:def 1;
    y = g3.x by A29,A30,FUNCT_1:47
      .= U1(r) by A26,A31
      .= dwa*r - 1;
    then y in {rr where rr is Real: 0 <= rr & rr <= 1} by A34,A35;
    hence thesis by BORSUK_1:40,RCOMP_1:def 1;
  end;
  then reconsider g4 = g39 as Function of T2,I[01] by A28,RELSET_1:4;
  [#] T1 = [. 0,1/2 .] & [#] T2 = [. 1/2,1 .] by TOPMETR:18;
  then
A36: ([#] T1) \/ ([#] T2) = [#](I[01] qua TopSpace) & ([#] T1) /\ ([#] T2) =
  {pp} by BORSUK_1:40,XXREAL_1:165,418;
A37: g3.x = 2*x + (-1)
  proof
   reconsider x as Element of REAL by XREAL_0:def 1;
    g3.x = U1(x) by A26
      .= dwa*x -1
      .= 2*x + (-1);
   hence thesis;
  end;
  R^1|PP = T2 by TOPMETR:19;
  then g39 is continuous by A37,TOPMETR:7,21;
  then
A38: g4 is continuous by PRE_TOPC:27;
A39: for x being object st x in [. 0,1/2 .] ex u being object st X[x,u]
  proof
    let x be object;
    assume x in [. 0,1/2 .];
    then x in { r: 0 <= r & r <= 1/2} by RCOMP_1:def 1;
    then consider r such that
A40: r=x and
    0<=r and
    r<=1/2;
    take f.(2*r);
    thus thesis by A40;
  end;
  consider f2 being Function such that
A41: dom f2 = [. 0,1/2 .] and
A42: for x being object st x in [. 0,1/2 .] holds X[x,f2.x] from CLASSES1:
  sch 1(A39);
A43: dom f2 = the carrier of T1 by A41,TOPMETR:18;
  f is Function of the carrier of I[01], the carrier of M|P9;
  then
A44: dom f = [. 0,1 .] by BORSUK_1:40,FUNCT_2:def 1;
  now
    let y be object;
    assume y in rng f2;
    then consider x being object such that
A45: x in dom f2 and
A46: y = f2.x by FUNCT_1:def 3;
    x in { a: 0 <= a & a <= 1/2 } by A41,A45,RCOMP_1:def 1;
    then consider a such that
A47: x = a and
A48: 0 <= a & a <= 1/2;
    0 <= 2*a & 2*a <= 2*(1/2) by A48,XREAL_1:64,127;
    then 2*a in { r: 0 <= r & r <= 1 };
    then
A49: 2*a in dom f by A44,RCOMP_1:def 1;
    y = f.(2*a) by A41,A42,A45,A46,A47;
    hence y in P by A15,A49,FUNCT_1:def 3;
  end;
  then
A50: rng f2 c= P;
  P c= P \/ Q by XBOOLE_1:7;
  then rng f2 c= the carrier of T|(P \/ Q qua Subset of T) by A11,A50;
  then reconsider f1 = f2 as Function of T1,M|R by A43,FUNCT_2:def 1,RELSET_1:4
;
  for x being object st x in the carrier of T1 holds f1.x = (ff*f4).x
  proof
    let x be object such that
A51: x in the carrier of T1;
    the carrier of T1 = [. 0,1/2 .] by TOPMETR:18;
    then reconsider x9=x as Element of REAL by A51;
    the carrier of T1 = [. 0,1/2 .] by TOPMETR:18;
    hence f1.x = f.(2*x9) by A42,A51
      .= f.U(x9)
      .= f.(f3.x9) by A10
      .= f.(f4.x) by A17,A51,FUNCT_1:47
      .= (ff*f4).x by A51,FUNCT_2:15;
  end;
  then
A52: f1 is continuous by A25,A16,FUNCT_2:12;
A53: now
    let x be Real;
    assume x in dom f2;
    then x in {a: 0 <= a & a <= 1/2} by A41,RCOMP_1:def 1;
    then consider a such that
A54: a=x and
A55: 0 <= a & a <= 1/2;
    0 <= 2*a & 2*a <= 2*(1/2) by A55,XREAL_1:64,127;
    then 2*a in { r: 0 <= r & r <= 1 };
    hence 2*x in dom f by A44,A54,RCOMP_1:def 1;
  end;
  defpred X[object,object] means for a st a=$1 holds $2 = g.(2*a-1);
A56: for x being object st x in [. 1/2,1 .] ex u being object st X[x,u]
  proof
    let x be object;
    assume x in [. 1/2,1 .];
    then x in { r: 1/2 <= r & r <= 1} by RCOMP_1:def 1;
    then consider r such that
A57: r=x and
    1/2<=r and
    r<=1;
    take g.(2*r-1);
    thus thesis by A57;
  end;
  consider g2 being Function such that
A58: dom g2 = [. 1/2, 1 .] and
A59: for x being object st x in [. 1/2,1 .] holds X[x,g2.x] from CLASSES1:
  sch 1(A56);
A60: dom g2 = the carrier of T2 by A58,TOPMETR:18;
  g is Function of the carrier of I[01], the carrier of M|Q9;
  then
A61: dom g = [. 0,1 .] by BORSUK_1:40,FUNCT_2:def 1;
  now
    let y be object;
    assume y in rng g2;
    then consider x being object such that
A62: x in dom g2 and
A63: y = g2.x by FUNCT_1:def 3;
    x in { a: 1/2 <= a & a <= 1 } by A58,A62,RCOMP_1:def 1;
    then consider a such that
A64: x = a and
A65: 1/2 <= a and
A66: a <= 1;
    2*a <= 2*1 by A66,XREAL_1:64;
    then
A67: 2*a-1 <= 1+1-1 by XREAL_1:9;
    2*(1/2) = 1;
    then 1 <= 2*a by A65,XREAL_1:64;
    then 1-1 <= 2*a-1 by XREAL_1:9;
    then 2*a -1 in { r: 0 <= r & r <= 1 } by A67;
    then
A68: 2*a -1 in dom g by A61,RCOMP_1:def 1;
    y = g.(2*a-1) by A58,A59,A62,A63,A64;
    hence y in Q by A8,A68,FUNCT_1:def 3;
  end;
  then
A69: rng g2 c= Q;
A70: Q c= rng g2
  proof
    let a be object;
    assume a in Q;
    then consider x being object such that
A71: x in dom g and
A72: a = g.x by A8,FUNCT_1:def 3;
    x in {r where r is Real: 0 <= r & r <= 1} by A61,A71,RCOMP_1:def 1;
    then consider x9 being Real such that
A73: x9 = x and
A74: 0 <= x9 and
A75: x9 <= 1;
    x9+1 <= 1+1 by A75,XREAL_1:6;
    then
A76: (x9+1)/2 <= 2/2 by XREAL_1:72;
    0+1 <= x9+1 by A74,XREAL_1:6;
    then 1/2 <= (x9+1)/2 by XREAL_1:72;
    then (x9+1)/2 in {r where r is Real: 1/2 <= r & r <= 1} by A76;
    then
A77: (x9+1)/2 in dom g2 by A58,RCOMP_1:def 1;
    a = g.(2*((x9+1)/2)-1) by A72,A73
      .= g2.((x9+1)/2) by A58,A59,A77;
    hence thesis by A77,FUNCT_1:def 3;
  end;
  TopSpaceMetr(RealSpace) is T_2 by PCOMPS_1:34;
  then
A78: I[01] is T_2 by TOPMETR:2,def 6;
A79: 1/2 in [. 1/2,1 .] by XXREAL_1:1;
A80: now
    let x be Real;
    assume x in dom g2;
    then x in {a: 1/2 <= a & a <= 1} by A58,RCOMP_1:def 1;
    then consider a such that
A81: a=x and
A82: 1/2 <= a and
A83: a <= 1;
    2*a <= 2*1 by A83,XREAL_1:64;
    then
A84: 2*a-1 <= 1+1-1 by XREAL_1:9;
    2*(1/2) = 1;
    then 1 <= 2*a by A82,XREAL_1:64;
    then 1-1 <= 2*a-1 by XREAL_1:9;
    then 2*a - 1 in { r: 0 <= r & r <= 1 } by A84;
    hence 2*x - 1 in dom g by A61,A81,RCOMP_1:def 1;
  end;
  Q c= P \/ Q by XBOOLE_1:7;
  then rng g2 c= the carrier of M|R by A11,A69;
  then reconsider g1 = g2 as Function of T2,M|R by A60,FUNCT_2:def 1,RELSET_1:4
;
  for x being object st x in the carrier of T2 holds g1.x = (g9*g4).x
  proof
    let x be object such that
A85: x in the carrier of T2;
    the carrier of T2 = [. 1/2,1 .] by TOPMETR:18;
    then reconsider x9=x as Element of REAL by A85;
    the carrier of T2 = [. 1/2,1 .] by TOPMETR:18;
    hence g1.x = g.(2*x9-1) by A59,A85
      .= g.U1(x9)
      .= g.(g3.x9) by A26
      .= g.(g4.x) by A27,A85,FUNCT_1:47
      .= (g9*g4).x by A85,FUNCT_2:15;
  end;
  then
A86: g1 is continuous by A38,A13,FUNCT_2:12;
  1/2 in [. 0,1/2 .] by XXREAL_1:1;
  then f1.pp = g.(2*(1/2) -1) by A5,A7,A42
    .= g1.pp by A59,A79;
  then reconsider
  h = f2 +* g2 as continuous Function of I[01],M|R by A36,A14,A78,A52,A86,
COMPTS_1:20;
A87: g is one-to-one by A6,TOPS_2:def 5;
A88: f is one-to-one by A4,TOPS_2:def 5;
  now
    let x1,x2 be object;
    assume that
A89: x1 in dom h and
A90: x2 in dom h and
A91: h.x1 = h.x2;
    now
      per cases;
      suppose
A92:    not x1 in dom g2 & not x2 in dom g2;
A93:    dom h = dom f2 \/ dom g2 by FUNCT_4:def 1;
        then x1 in [. 0,1/2 .] by A41,A89,A92,XBOOLE_0:def 3;
        then x1 in { a: 0 <= a & a <= 1/2 } by RCOMP_1:def 1;
        then consider x19 being Real such that
A94:    x19 = x1 and
        0 <= x19 and
        x19 <= 1/2;
        reconsider x19 as Real;
A95:    x1 in dom f2 by A89,A92,A93,XBOOLE_0:def 3;
        then
A96:    2*x19 in dom f by A53,A94;
        x2 in [. 0,1/2 .] by A41,A90,A92,A93,XBOOLE_0:def 3;
        then x2 in { a: 0 <= a & a <= 1/2 } by RCOMP_1:def 1;
        then consider x29 being Real such that
A97:    x29 = x2 and
        0 <= x29 and
        x29 <= 1/2;
        reconsider x29 as Real;
A98:    x2 in dom f2 by A90,A92,A93,XBOOLE_0:def 3;
        then
A99:    2*x29 in dom f by A53,A97;
        f.(2*x19) = f2.x1 by A41,A42,A95,A94
          .= h.x2 by A91,A92,FUNCT_4:11
          .= f2.x2 by A92,FUNCT_4:11
          .= f.(2*x29) by A41,A42,A98,A97;
        then 2*x19 = 2*x29 by A88,A96,A99,FUNCT_1:def 4;
        hence x1 = x2 by A94,A97;
      end;
      suppose
A100:   not x1 in dom g2 & x2 in dom g2;
        dom h = dom f2 \/ dom g2 by FUNCT_4:def 1;
        then
A101:   x1 in dom f2 by A89,A100,XBOOLE_0:def 3;
        then x1 in { a: 0 <= a & a <= 1/2 } by A41,RCOMP_1:def 1;
        then consider x19 being Real such that
A102:   x19 = x1 and
        0 <= x19 and
        x19 <= 1/2;
        reconsider x19 as Real;
A103:   2*x19 in dom f by A53,A101,A102;
        then
A104:   f.(2*x19) in P by A15,FUNCT_1:def 3;
        x2 in { a: 1/2 <= a & a <= 1 } by A58,A100,RCOMP_1:def 1;
        then consider x29 being Real such that
A105:   x29 = x2 and
        1/2 <= x29 and
        x29 <= 1;
        reconsider x29 as Real;
A106:   2*x29 -1 in dom g by A80,A100,A105;
        then
A107:   g.(2*x29 -1) in Q by A8,FUNCT_1:def 3;
A108:   1 in dom f by A44,XXREAL_1:1;
A109:   0 in dom g by A61,XXREAL_1:1;
A110:   f.(2*x19) = f2.x1 by A41,A42,A101,A102
          .= h.x2 by A91,A100,FUNCT_4:11
          .= g2.x2 by A100,FUNCT_4:13
          .= g.(2*x29 -1) by A58,A59,A100,A105;
        then g.(2*x29 -1) in P /\ Q by A104,A107,XBOOLE_0:def 4;
        then g.(2*x29 -1) = p by A3,TARSKI:def 1;
        then
A111:   2*x29-1+1 = 0+1 by A7,A87,A106,A109,FUNCT_1:def 4;
        f.(2*x19) in P /\ Q by A110,A104,A107,XBOOLE_0:def 4;
        then f.(2*x19) = p by A3,TARSKI:def 1;
        then 1/2*(2*x19) = 1/2*1 by A5,A88,A103,A108,FUNCT_1:def 4;
        hence x1 = x2 by A105,A102,A111;
      end;
      suppose
A112:   x1 in dom g2 & not x2 in dom g2;
        dom h = dom f2 \/ dom g2 by FUNCT_4:def 1;
        then
A113:   x2 in dom f2 by A90,A112,XBOOLE_0:def 3;
        then x2 in { a: 0 <= a & a <= 1/2 } by A41,RCOMP_1:def 1;
        then consider x29 being Real such that
A114:   x29 = x2 and
        0 <= x29 and
        x29 <= 1/2;
        reconsider x29 as Real;
A115:   2*x29 in dom f by A53,A113,A114;
        then
A116:   f.(2*x29) in P by A15,FUNCT_1:def 3;
        x1 in { a: 1/2 <= a & a <= 1 } by A58,A112,RCOMP_1:def 1;
        then consider x19 being Real such that
A117:   x19 = x1 and
        1/2 <= x19 and
        x19 <= 1;
        reconsider x19 as Real;
A118:   2*x19 -1 in dom g by A80,A112,A117;
        then
A119:   g.(2*x19 -1) in Q by A8,FUNCT_1:def 3;
A120:   1 in dom f by A44,XXREAL_1:1;
A121:   0 in dom g by A61,XXREAL_1:1;
A122:   f.(2*x29) = f2.x2 by A41,A42,A113,A114
          .= h.x1 by A91,A112,FUNCT_4:11
          .= g2.x1 by A112,FUNCT_4:13
          .= g.(2*x19 -1) by A58,A59,A112,A117;
        then g.(2*x19 -1) in P /\ Q by A116,A119,XBOOLE_0:def 4;
        then g.(2*x19 -1) = p by A3,TARSKI:def 1;
        then
A123:   2*x19-1+1 = 0+1 by A7,A87,A118,A121,FUNCT_1:def 4;
        f.(2*x29) in P /\ Q by A122,A116,A119,XBOOLE_0:def 4;
        then f.(2*x29) = p by A3,TARSKI:def 1;
        then 1/2*(2*x29) = 1/2*1 by A5,A88,A115,A120,FUNCT_1:def 4;
        hence x1 = x2 by A117,A114,A123;
      end;
      suppose
A124:   x1 in dom g2 & x2 in dom g2;
        then x2 in { a: 1/2 <= a & a <= 1 } by A58,RCOMP_1:def 1;
        then consider x29 being Real such that
A125:   x29 = x2 and
        1/2 <= x29 and
        x29 <= 1;
        reconsider x29 as Real;
A126:   2*x29-1 in dom g by A80,A124,A125;
        x1 in { a: 1/2 <= a & a <= 1 } by A58,A124,RCOMP_1:def 1;
        then consider x19 being Real such that
A127:   x19 = x1 and
        1/2 <= x19 and
        x19 <= 1;
        reconsider x19 as Real;
A128:   2*x19-1 in dom g by A80,A124,A127;
        g.(2*x19-1) = g2.x1 by A58,A59,A124,A127
          .= h.x2 by A91,A124,FUNCT_4:13
          .= g2.x2 by A124,FUNCT_4:13
          .= g.(2*x29-1) by A58,A59,A124,A125;
        then 2*x19 - 1 + 1 = 2*x29 - 1 + 1 by A87,A128,A126,FUNCT_1:def 4;
        hence x1 = x2 by A127,A125;
      end;
    end;
    hence x1 = x2;
  end;
  then
A129: dom h = [#]I[01] & h is one-to-one by FUNCT_1:def 4,FUNCT_2:def 1;
  reconsider h9 = h as Function of I[01],T|(P \/ Q);
  take h9;
A130: 0 in [. 0,1/2 .] by XXREAL_1:1;
A131: P c= rng f2
  proof
    let a be object;
    assume a in P;
    then consider x being object such that
A132: x in dom f and
A133: a = f.x by A15,FUNCT_1:def 3;
    x in {r where r is Real: 0 <= r & r <= 1} by A44,A132,RCOMP_1:def 1;
    then consider x9 being Real such that
A134: x9 = x and
A135: 0 <= x9 & x9 <= 1;
        reconsider x9 as Real;
    0/2 <= x9/2 & x9/2 <= 1/2 by A135,XREAL_1:72;
    then x9/2 in {r where r is Real: 0 <= r & r <= 1/2};
    then
A136: x9/2 in dom f2 by A41,RCOMP_1:def 1;
    a = f.(2*(x9/2)) by A133,A134
      .= f2.(x9/2) by A41,A42,A136;
    hence thesis by A136,FUNCT_1:def 3;
  end;
A137: P c= rng h
  proof
    let a be object;
    assume a in P;
    then consider x being object such that
A138: x in dom f2 and
A139: a = f2.x by A131,FUNCT_1:def 3;
    now
      per cases;
      suppose
A140:   x in [. 1/2,1 .];
        then x in [. 0,1/2 .] /\ [. 1/2,1 .] by A41,A138,XBOOLE_0:def 4;
        then x in {1/2} by XXREAL_1:418;
        then
A141:   x = 1/2 by TARSKI:def 1;
        x in dom f2 \/ dom g2 by A138,XBOOLE_0:def 3;
        then
A142:   x in dom h by FUNCT_4:def 1;
A143:   1/2 in [. 0,1/2 .] by XXREAL_1:1;
        h.x = g2.x by A58,A140,FUNCT_4:13
          .= g.(2*(1/2) - 1) by A59,A140,A141
          .= f2.(1/2) by A5,A7,A42,A143;
        hence thesis by A139,A141,A142,FUNCT_1:def 3;
      end;
      suppose
A144:   not x in [. 1/2,1 .];
A145:   x in dom f2 \/ dom g2 by A138,XBOOLE_0:def 3;
        then
A146:   x in dom h by FUNCT_4:def 1;
        h.x = f2.x by A58,A144,A145,FUNCT_4:def 1;
        hence thesis by A139,A146,FUNCT_1:def 3;
      end;
    end;
    hence thesis;
  end;
  rng h c= rng f2 \/ rng g2 & rng f2 \/ rng g2 c= P \/ Q by A50,A69,FUNCT_4:17
,XBOOLE_1:13;
  then
A147: rng h c= P \/ Q;
  rng g2 c= rng h by FUNCT_4:18;
  then Q c= rng h by A70;
  then P \/ Q c= rng h by A137,XBOOLE_1:8;
  then rng h = P \/ Q by A147,XBOOLE_0:def 10;
  then
A148: rng h = [#] (M|R) by PRE_TOPC:def 5;
  I[01] is compact & M|R is T_2 by HEINE:4,TOPMETR:2,20;
  hence h9 is being_homeomorphism by A148,A129,COMPTS_1:17;
  not 0 in dom g2 by A58,XXREAL_1:1;
  hence h9.0 = f2.0 by FUNCT_4:11
    .= f.(2*0) by A42,A130
    .= f.0;
A149: 1 in dom g2 by A58,XXREAL_1:1;
  hence h9.1 = g2.1 by FUNCT_4:13
    .= g.(2*1-1) by A58,A59,A149
    .= g.1;
end;