TOPREALA

:: Some Properties of Rectangles on the Plane
::  by Artur Korni{\l}owicz and Yasunari Shidama
::
:: Received October 18, 2004
:: Copyright (c) 2004-2026 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, STRUCT_0, TOPMETR, ZFMISC_1, INT_1, ARYTM_3, ARYTM_1,
      XXREAL_0, XXREAL_1, XBOOLE_0, CARD_1, FUNCT_1, RELAT_1, FINSEQ_1, CARD_3,
      FUNCOP_1, MONOID_0, PRE_TOPC, PCOMPS_1, EUCLID, SUBSET_1, RCOMP_1,
      CONNSP_2, TOPS_1, TARSKI, NATTRA_1, TDLAT_3, ORDINAL2, FUNCT_2, T_0TOPSP,
      TOPS_2, PARTFUN1, REAL_1, FCONT_1, TMAP_1, JGRAPH_6, MCART_1, TOPREALA,
      NAT_1;
 notations TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, ORDINAL1, RELAT_1, FUNCT_1,
      RELSET_1, PARTFUN1, FUNCT_2, NUMBERS, XCMPLX_0, XXREAL_0, XREAL_0,
      REAL_1, FUNCOP_1, INT_1, CARD_3, FINSEQ_1, FUNCT_4, MONOID_0, RCOMP_1,
      FCONT_1, STRUCT_0, PRE_TOPC, PCOMPS_1, TOPS_1, BORSUK_1, TSEP_1, TOPS_2,
      TDLAT_3, CONNSP_2, T_0TOPSP, TMAP_1, TOPMETR, EUCLID, JGRAPH_6;
 constructors FUNCT_4, REAL_1, CARD_3, RCOMP_1, FINSEQ_4, FCONT_1, TOPS_1,
      TOPS_2, TDLAT_3, TMAP_1, T_0TOPSP, MONOID_0, BORSUK_4, JGRAPH_6,
      FUNCSDOM, PCOMPS_1;
 registrations RELSET_1, FUNCT_2, FUNCT_4, NUMBERS, XXREAL_0, XREAL_0,
      MEMBERED, FINSEQ_1, STRUCT_0, PRE_TOPC, TOPS_1, BORSUK_1, TSEP_1,
      MONOID_0, EUCLID, TOPMETR, TOPGRP_1, VALUED_0, FCONT_1, PCOMPS_1,
      FUNCT_1, RELAT_1, ORDINAL1;
 requirements NUMERALS, BOOLE, SUBSET, ARITHM, REAL;
 definitions TARSKI, XBOOLE_0, FUNCT_2, PRE_TOPC, T_0TOPSP, TMAP_1, STRUCT_0,
      RCOMP_1, FCONT_1, MONOID_0, PARTFUN2;
 equalities XBOOLE_0, TMAP_1, STRUCT_0, RCOMP_1, EUCLID;
 expansions TARSKI, XBOOLE_0, FUNCT_2, T_0TOPSP, FCONT_1;
 theorems PRE_TOPC, XREAL_0, FUNCT_2, BORSUK_1, EUCLID, TOPS_2, BORSUK_3,
      FUNCT_1, TOPMETR, RELAT_1, FUNCOP_1, TOPREAL6, JORDAN16, BORSUK_6,
      TARSKI, ZFMISC_1, FUNCT_4, TSEP_1, HILBERT3, FINSEQ_1, TMAP_1, XBOOLE_1,
      JORDAN6, TOPS_3, FCONT_1, CONNSP_2, FRECHET, XBOOLE_0, FINSEQ_3, NAT_1,
      RCOMP_1, TEX_2, DOMAIN_1, TOPS_1, TOPGRP_1, TREAL_1, CARD_3, JGRAPH_6,
      TDLAT_3, ENUMSET1, TOPALG_3, XREAL_1, XXREAL_0, XXREAL_1;

begin :: Subsets of REAL

set R = the carrier of R^1;

Lm1: the carrier of [:R^1,R^1:] = [:R,R:] by BORSUK_1:def 2;

reserve i for Integer,
  a, b, r, s for Real;

registration
  let r be Real, s be positive Real;
  cluster ].r,r+s.[ -> non empty;
  coherence
  proof
    r+0 < r+s by XREAL_1:6;
    then r < (r+(r+s))/2 & (r+(r+s))/2 < r+s by XREAL_1:226;
    hence thesis by XXREAL_1:4;
  end;
  cluster [.r,r+s.[ -> non empty;
  coherence
  proof
    r+0 < r+s by XREAL_1:6;
    hence thesis by XXREAL_1:3;
  end;
  cluster ].r,r+s.] -> non empty;
  coherence
  proof
    r+0 < r+s by XREAL_1:6;
    hence thesis by XXREAL_1:2;
  end;
  cluster [.r,r+s.] -> non empty;
  coherence
  proof
    r+0 < r+s by XREAL_1:6;
    hence thesis by XXREAL_1:1;
  end;
  cluster ].r-s,r.[ -> non empty;
  coherence
  proof
    r-s < r-0 by XREAL_1:15;
    then r-s < (r-s+r)/2 & (r-s+r)/2 < r by XREAL_1:226;
    hence thesis by XXREAL_1:4;
  end;
  cluster [.r-s,r.[ -> non empty;
  coherence
  proof
    r-s < r-0 by XREAL_1:15;
    hence thesis by XXREAL_1:3;
  end;
  cluster ].r-s,r.] -> non empty;
  coherence
  proof
    r-s < r-0 by XREAL_1:15;
    hence thesis by XXREAL_1:32;
  end;
  cluster [.r-s,r.] -> non empty;
  coherence
  proof
    r-s < r-0 by XREAL_1:15;
    hence thesis by XXREAL_1:1;
  end;
end;

registration
  let r be non positive Real, s be positive Real;
  cluster ].r,s.[ -> non empty;
  coherence
  proof
    r < (r+s)/2 & (r+s)/2 < s by XREAL_1:226;
    hence thesis by XXREAL_1:4;
  end;
  cluster [.r,s.[ -> non empty;
  coherence by XXREAL_1:3;
  cluster ].r,s.] -> non empty;
  coherence by XXREAL_1:2;
  cluster [.r,s.] -> non empty;
  coherence by XXREAL_1:1;
end;

registration
  let r be negative Real, s be non negative Real;
  cluster ].r,s.[ -> non empty;
  coherence
  proof
    r < (r+s)/2 & (r+s)/2 < s by XREAL_1:226;
    hence thesis by XXREAL_1:4;
  end;
  cluster [.r,s.[ -> non empty;
  coherence by XXREAL_1:3;
  cluster ].r,s.] -> non empty;
  coherence by XXREAL_1:2;
  cluster [.r,s.] -> non empty;
  coherence by XXREAL_1:1;
end;

begin :: Functions

theorem
  for f being Function, x, X being set st x in dom f & f.x in f.:X & f
  is one-to-one holds x in X
proof
  let f be Function, x, X be set;
  assume
A1: x in dom f;
  assume f.x in f.:X;
  then
A2: ex a being object st a in dom f & a in X & f.x = f.a by FUNCT_1:def 6;
  assume f is one-to-one;
  hence thesis by A1,A2,FUNCT_1:def 4;
end;

theorem
  for f being FinSequence, i being Nat st i+1 in dom f holds
  i in dom f or i = 0
proof
  let f be FinSequence;
  let i be Nat;
  assume
A1: i+1 in dom f;
  then 1 <= i+1 by FINSEQ_3:25;
  then
A2: 1 < i+1 or 1+0 = i+1 by XXREAL_0:1;
  per cases by A2,NAT_1:13;
  suppose
    i = 0;
    hence thesis;
  end;
  suppose
A3: 1 <= i;
    i+1 <= len f by A1,FINSEQ_3:25;
    then i <= len f by NAT_1:13;
    hence thesis by A3,FINSEQ_3:25;
  end;
end;

theorem Th3:
  for x, y, X, Y being set, f being Function st x <> y & f in
  product ((x,y) --> (X,Y)) holds f.x in X & f.y in Y
proof
  let x, y, X, Y be set, f be Function such that
A1: x <> y and
A2: f in product ((x,y) --> (X,Y));
  set g = (x,y) --> (X,Y);
A3: dom g = {x,y} by FUNCT_4:62;
  then y in dom g by TARSKI:def 2;
  then
A4: f.y in g.y by A2,CARD_3:9;
  x in dom g by A3,TARSKI:def 2;
  then f.x in g.x by A2,CARD_3:9;
  hence thesis by A1,A4,FUNCT_4:63;
end;

theorem Th4:
  for a, b being object holds <*a,b*> = (1,2) --> (a,b)
proof
  let a, b be object;
  set f = (1,2) --> (a,b);
  set g = <*a,b*>;
A1: dom f = {1,2} by FUNCT_4:62;
A2: now
    let x be object;
    assume
A3: x in dom f;
    per cases by A1,A3,TARSKI:def 2;
    suppose
A4:   x = 1;
      hence f.x = a by FUNCT_4:63
        .= g.x by A4;
    end;
    suppose
A5:   x = 2;
      hence f.x = b by FUNCT_4:63
        .= g.x by A5;
    end;
  end;
  dom g = {1,2} by FINSEQ_1:2,89;
  hence thesis by A2,FUNCT_1:2,FUNCT_4:62;
end;

begin :: General topology

registration
  cluster constituted-FinSeqs non empty strict for TopSpace;
  existence
  proof
    take T=TopSpaceMetr Euclid 1;
    thus for a being Element of T holds a is FinSequence
    proof
      let a be Element of T;
      T = the TopStruct of TOP-REAL 1 by EUCLID:def 8;
      hence a is FinSequence;
    end;
    thus thesis;
  end;
end;

registration
  let T be constituted-FinSeqs TopSpace;
  cluster -> constituted-FinSeqs for SubSpace of T;
  coherence
  proof
    let X be SubSpace of T;
    let p be Element of X;
A1: the carrier of X is Subset of T by TSEP_1:1;
    per cases;
    suppose
      the carrier of X is non empty;
      then p in the carrier of X;
      then reconsider p as Point of T by A1;
      p is FinSequence;
      hence thesis;
    end;
    suppose
      the carrier of X is empty;
      hence thesis;
    end;
  end;
end;

theorem Th5:
  for T being non empty TopSpace, Z being non empty SubSpace of T,
  t being Point of T, z being Point of Z, N being open a_neighborhood of t, M
being Subset of Z st t = z & M = N /\ [#]Z holds M is open a_neighborhood of z
proof
  let T be non empty TopSpace, Z be non empty SubSpace of T, t be Point of T,
  z be Point of Z, N be open a_neighborhood of t, M be Subset of Z such that
A1: t = z and
A2: M = N /\ [#]Z;
  M is open by A2,TOPS_2:24;
  then
A3: Int M = M by TOPS_1:23;
  t in Int N & Int N c= N by CONNSP_2:def 1,TOPS_1:16;
  then z in Int M by A1,A2,A3,XBOOLE_0:def 4;
  hence thesis by A2,CONNSP_2:def 1,TOPS_2:24;
end;

registration
  cluster empty -> discrete anti-discrete for TopSpace;
  coherence
  proof
    let T be TopSpace;
    assume T is empty;
    then the carrier of T = {};
    then bool the carrier of T = {{}, the carrier of T} by ENUMSET1:29
,ZFMISC_1:1;
    hence thesis by TDLAT_3:14;
  end;
end;

registration
  let X be discrete TopSpace, Y be TopSpace;
  cluster -> continuous for Function of X,Y;
  coherence by TEX_2:62;
end;

theorem Th6:
  for X being TopSpace, Y being TopStruct, f being Function of X,Y
  st f is empty holds f is continuous
proof
  let X be TopSpace, Y be TopStruct, f be Function of X,Y such that
A1: f is empty;
  let P being Subset of Y;
  assume P is closed;
  f"P = {}X by A1;
  hence thesis;
end;

registration
  let X be TopSpace, Y be TopStruct;
  cluster empty -> continuous for Function of X,Y;
  coherence by Th6;
end;

theorem
  for X being TopStruct, Y being non empty TopStruct, Z being non empty
  SubSpace of Y, f being Function of X,Z holds f is Function of X,Y
proof
  let X be TopStruct, Y be non empty TopStruct, Z be non empty SubSpace of Y;
  let f be Function of X,Z;
  the carrier of Z is Subset of Y by TSEP_1:1;
  then
A1: rng f c= the carrier of Y by XBOOLE_1:1;
  dom f = the carrier of X by FUNCT_2:def 1;
  hence thesis by A1,FUNCT_2:2;
end;

theorem
  for S, T being non empty TopSpace, X being Subset of S, Y being Subset
of T, f being continuous Function of S,T, g being Function of S|X,T|Y st g = f|
  X holds g is continuous
proof
  let S, T be non empty TopSpace, X be Subset of S, Y be Subset of T, f be
  continuous Function of S,T, g be Function of S|X,T|Y such that
A1: g = f|X;
  set h = f|X;
A2: the carrier of S|X = X & rng h c= the carrier of T by PRE_TOPC:8;
  dom f = the carrier of S by FUNCT_2:def 1;
  then dom h = X by RELAT_1:62;
  then reconsider h as Function of S|X,T by A2,FUNCT_2:2;
  h is continuous by TOPMETR:7;
  hence thesis by A1,TOPMETR:6;
end;

theorem
  for S, T being non empty TopSpace, Z being non empty SubSpace of T, f
being Function of S,T, g being Function of S,Z st f = g & f is open holds g is
  open
proof
  let S, T be non empty TopSpace, Z be non empty SubSpace of T, f be Function
  of S,T, g be Function of S,Z such that
A1: f = g and
A2: f is open;
  for p being Point of S, P being open a_neighborhood of p ex R being
  a_neighborhood of g.p st R c= g.:P
  proof
    let p be Point of S, P be open a_neighborhood of p;
    consider R being open a_neighborhood of f.p such that
A3: R c= f.:P by A2,TOPGRP_1:22;
    reconsider R2 = R /\ [#]Z as Subset of Z;
    reconsider R2 as a_neighborhood of g.p by A1,Th5;
    take R2;
    R2 c= R by XBOOLE_1:17;
    hence thesis by A1,A3;
  end;
  hence thesis by TOPGRP_1:23;
end;

theorem
  for S, T being non empty TopSpace, S1 being Subset of S, T1 being
Subset of T, f being Function of S,T, g being Function of S|S1,T|T1 st g = f|S1
  & g is onto & f is open one-to-one holds g is open
proof
  let S, T be non empty TopSpace, S1 be Subset of S, T1 be Subset of T, f be
  Function of S,T, g be Function of S|S1,T|T1 such that
A1: g = f|S1 and
A2: rng g = the carrier of T|T1 and
A3: f is open and
A4: f is one-to-one;
  let A be Subset of S|S1;
A5: [#](T|T1)= T1 by PRE_TOPC:def 5;
  assume A is open;
  then consider C being Subset of S such that
A6: C is open and
A7: C /\ [#](S|S1) = A by TOPS_2:24;
A8: [#](S|S1)= S1 & g.:(C /\ S1) c= g.:C /\ g.:S1 by PRE_TOPC:def 5,RELAT_1:121
;
A9: g.:A = (f.:C) /\ T1
  proof
    g.:C c= f.:C by A1,RELAT_1:128;
    then g.:C /\ g.:S1 c= (f.:C) /\ T1 by A5,XBOOLE_1:27;
    hence g.:A c= (f.:C) /\ T1 by A7,A8;
    let y be object;
A10: dom g c= dom f & dom f = the carrier of S by A1,FUNCT_2:def 1,RELAT_1:60;
    assume
A11: y in (f.:C) /\ T1;
    then y in f.:C by XBOOLE_0:def 4;
    then consider x being Element of S such that
A12: x in C and
A13: y = f.x by FUNCT_2:65;
    y in T1 by A11,XBOOLE_0:def 4;
    then consider a being object such that
A14: a in dom g and
A15: g.a = y by A2,A5,FUNCT_1:def 3;
    f.a = g.a by A1,A14,FUNCT_1:47;
    then a = x by A4,A13,A14,A15,A10,FUNCT_1:def 4;
    then a in A by A7,A12,A14,XBOOLE_0:def 4;
    hence thesis by A14,A15,FUNCT_1:def 6;
  end;
  f.:C is open by A3,A6;
  hence thesis by A5,A9,TOPS_2:24;
end;

theorem
  for X, Y, Z being non empty TopSpace, f being Function of X,Y, g being
  Function of Y,Z st f is open & g is open holds g*f is open
proof
  let X, Y, Z be non empty TopSpace, f be Function of X,Y, g be Function of Y,
  Z such that
A1: f is open and
A2: g is open;
  let A be Subset of X;
  assume A is open;
  then
A3: f.:A is open by A1;
  (g*f).:A = g.:(f.:A) by RELAT_1:126;
  hence thesis by A2,A3;
end;

theorem
  for X, Y being TopSpace, Z being open SubSpace of Y, f being Function
  of X, Y, g being Function of X, Z st f = g & g is open holds f is open
proof
  let X, Y be TopSpace, Z be open SubSpace of Y, f be Function of X, Y, g be
  Function of X, Z such that
A1: f = g and
A2: g is open;
  let A be Subset of X;
  assume A is open;
  then g.:A is open by A2;
  hence thesis by A1,TSEP_1:17;
end;

theorem Th13:
  for S, T being non empty TopSpace, f being Function of S,T st f
  is one-to-one onto holds f is continuous iff f" is open
proof
  let S, T be non empty TopSpace, f be Function of S,T such that
A1: f is one-to-one;
  assume f is onto;
  then
A2: f qua Function" = f" by A1,TOPS_2:def 4;
A3: [#]T <> {};
  thus f is continuous implies f" is open
  proof
    assume
A4: f is continuous;
    let A be Subset of T;
    assume A is open;
    then f"A is open by A3,A4,TOPS_2:43;
    hence thesis by A1,A2,FUNCT_1:85;
  end;
  assume
A5: f" is open;
  now
    let A be Subset of T;
    assume A is open;
    then f".:A is open by A5;
    hence f"A is open by A1,A2,FUNCT_1:85;
  end;
  hence thesis by A3,TOPS_2:43;
end;

theorem
  for S, T being non empty TopSpace, f being Function of S,T st f is
  one-to-one onto holds f is open iff f" is continuous
proof
  let S, T be non empty TopSpace, f be Function of S,T such that
A1: f is one-to-one;
  assume f is onto;
  then
A2: rng f = [#]T;
  then rng (f") = [#]S by A1,TOPS_2:49;
  then
A3: f" is onto;
  f" is one-to-one & f"" = f by A1,A2,TOPS_2:50,51;
  hence thesis by A3,Th13;
end;

theorem
  for S being TopSpace, T being non empty TopSpace holds S,T
  are_homeomorphic iff the TopStruct of S, the TopStruct of T are_homeomorphic
proof
  let S be TopSpace, T be non empty TopSpace;
  set SS = the TopStruct of S;
  set TT = the TopStruct of T;
A1: [#]S = [#]SS & [#]T = [#]TT;
  thus S,T are_homeomorphic implies the TopStruct of S, the TopStruct of T
  are_homeomorphic
  proof
    given f being Function of S,T such that
A2: f is being_homeomorphism;
    reconsider g = f as Function of SS,TT;
A3: now
      let P be Subset of SS;
      reconsider R = P as Subset of S;
      thus g.:(Cl P) = f.:(Cl R) by TOPS_3:80
        .= Cl(f.:R) by A2,TOPS_2:60
        .= Cl(g.:P) by TOPS_3:80;
    end;
    take g;
    dom f = [#]S & rng f = [#]T by A2,TOPS_2:60;
    hence thesis by A1,A2,A3,TOPS_2:60;
  end;
  given f being Function of SS,TT such that
A4: f is being_homeomorphism;
  reconsider g = f as Function of S,T;
A5: now
    let P be Subset of S;
    reconsider R = P as Subset of SS;
    thus g.:(Cl P) = f.:(Cl R) by TOPS_3:80
      .= Cl(f.:R) by A4,TOPS_2:60
      .= Cl(g.:P) by TOPS_3:80;
  end;
  take g;
  dom f = [#]SS & rng f = [#]TT by A4,TOPS_2:60;
  hence thesis by A1,A4,A5,TOPS_2:60;
end;

theorem
  for S, T being non empty TopSpace, f being Function of S,T st f is
  one-to-one onto continuous open holds f is being_homeomorphism
proof
  let S, T be non empty TopSpace, f be Function of S,T such that
A1: f is one-to-one and
A2: f is onto and
A3: f is continuous and
A4: f is open;
A5: [#]T <> {};
A6: dom f = the carrier of S by FUNCT_2:def 1;
A7: for P being Subset of S holds P is open iff f.:P is open
  proof
    let P be Subset of S;
    thus P is open implies f.:P is open by A4;
    assume f.:P is open;
    then f"(f.:P) is open by A3,A5,TOPS_2:43;
    hence thesis by A1,A6,FUNCT_1:94;
  end;
  dom f = [#]S & rng f = [#]T by A2,FUNCT_2:def 1;
  hence thesis by A1,A7,TOPGRP_1:25;
end;

begin :: R^1

theorem
  for f being PartFunc of REAL,REAL st f = REAL --> r holds f|REAL is
  continuous
proof
  let f be PartFunc of REAL,REAL such that
A1: f = REAL --> r;
  f|REAL is constant
  proof
    reconsider r as Element of REAL by XREAL_0:def 1;
    take r;
    let c be Element of REAL;
    assume c in dom(f|REAL);
    thus (f|REAL).c = f.c
      .= r by A1,FUNCOP_1:7;
  end;
  hence thesis;
end;

theorem
  for f, f1, f2 being PartFunc of REAL,REAL st dom f = dom f1 \/ dom f2
  & dom f1 is open & dom f2 is open & f1|dom f1 is continuous & f2|dom f2 is
  continuous & (for z being set st z in dom f1 holds f.z = f1.z) & (for z being
  set st z in dom f2 holds f.z = f2.z) holds f|dom f is continuous
proof
  let f, f1, f2 be PartFunc of REAL,REAL;
  set X1 = dom f1, X2 = dom f2;
  assume that
A1: dom f = X1 \/ X2 and
A2: X1 is open and
A3: X2 is open and
A4: f1|X1 is continuous and
A5: f2|X2 is continuous and
A6: for z being set st z in X1 holds f.z = f1.z and
A7: for z being set st z in X2 holds f.z = f2.z;
A8: dom f /\ X1 = X1 by A1,XBOOLE_1:7,28;
A9: dom (f|X2) = dom f /\ X2 by RELAT_1:61;
  let x be Real;
  assume x in dom(f|dom f);
  then
A10: x in dom f;
A11: (f|(X1 \/ X2)).x = f.x by A1;
A12: dom f /\ X2 = X2 by A1,XBOOLE_1:7,28;
A13: dom (f|X1) = dom f /\ X1 by RELAT_1:61;
  per cases by A1,A10,XBOOLE_0:def 3;
  suppose
A14: x in X1;
    then
A15: (f|(X1 \/ X2)).x = f1.x by A6,A11
      .= (f1|X1).x;
    for N1 being Neighbourhood of (f|(X1 \/ X2)).x ex N being
Neighbourhood of x st for x1 being Real st x1 in dom (f|(X1 \/ X2)) & x1
    in N holds (f|(X1 \/ X2)).x1 in N1
    proof
      let N1 be Neighbourhood of (f|(X1 \/ X2)).x;
      consider N2 being Neighbourhood of x such that
A16:  N2 c= X1 by A2,A14,RCOMP_1:18;
      x in dom(f1|X1) by A14;
      then f1|X1 is_continuous_in x by A4;
      then consider N being Neighbourhood of x such that
A17:  for x1 being Real st x1 in dom (f1|X1) & x1 in N holds (
      f1|X1).x1 in N1 by A15,FCONT_1:4;
      consider N3 being Neighbourhood of x such that
A18:  N3 c= N and
A19:  N3 c= N2 by RCOMP_1:17;
      take N3;
      let x1 be Real such that
A20:  x1 in dom (f|(X1 \/ X2)) and
A21:  x1 in N3;
      per cases;
      suppose
A22:    x1 in dom (f|X1);
A23:    dom (f|X1) = X1 /\ X1 by A1,A13,XBOOLE_1:7,28
          .= dom (f1|X1);
A24:    x1 in X1 by A13,A22,XBOOLE_0:def 4;
        (f|(X1 \/ X2)).x1 = f.x1 by A20,FUNCT_1:47
          .= f1.x1 by A6,A24
          .= (f1|X1).x1;
        hence thesis by A17,A18,A21,A22,A23;
      end;
      suppose
A25:    not x1 in dom (f|X1);
        x1 in N2 by A19,A21;
        hence thesis by A13,A8,A16,A25;
      end;
    end;
    hence thesis by A1,FCONT_1:4;
  end;
  suppose
A26: x in X2;
    then
A27: (f|(X1 \/ X2)).x = f2.x by A7,A11
      .= (f2|X2).x;
    for N1 being Neighbourhood of (f|(X1 \/ X2)).x ex N being
Neighbourhood of x st for x1 being Real st x1 in dom (f|(X1 \/ X2)) & x1
    in N holds (f|(X1 \/ X2)).x1 in N1
    proof
      let N1 be Neighbourhood of (f|(X1 \/ X2)).x;
      consider N2 being Neighbourhood of x such that
A28:  N2 c= X2 by A3,A26,RCOMP_1:18;
      x in dom(f2|X2) by A26;
      then f2|X2 is_continuous_in x by A5;
      then consider N being Neighbourhood of x such that
A29:  for x1 being Real st x1 in dom (f2|X2) & x1 in N holds (
      f2|X2).x1 in N1 by A27,FCONT_1:4;
      consider N3 being Neighbourhood of x such that
A30:  N3 c= N and
A31:  N3 c= N2 by RCOMP_1:17;
      take N3;
      let x1 be Real such that
A32:  x1 in dom (f|(X1 \/ X2)) and
A33:  x1 in N3;
      per cases;
      suppose
A34:    x1 in dom (f|X2);
A35:    dom (f|X2) = X2 /\ X2 by A1,A9,XBOOLE_1:7,28
          .= dom (f2|X2);
A36:    x1 in X2 by A9,A34,XBOOLE_0:def 4;
        (f|(X1 \/ X2)).x1 = f.x1 by A32,FUNCT_1:47
          .= f2.x1 by A7,A36
          .= (f2|X2).x1;
        hence thesis by A29,A30,A33,A34,A35;
      end;
      suppose
A37:    not x1 in dom (f|X2);
        x1 in N2 by A31,A33;
        hence thesis by A9,A12,A28,A37;
      end;
    end;
    hence thesis by A1,FCONT_1:4;
  end;
end;

theorem Th19:
  for x being Point of R^1, N being Subset of REAL, M being Subset
of R^1 st M = N holds N is Neighbourhood of x implies M is a_neighborhood of x
proof
  let x be Point of R^1, N be Subset of REAL, M be Subset of R^1 such that
A1: M = N;
  given r such that
A2: 0 < r and
A3: N = ].x-r,x+r.[;
  M is open by A1,A3,JORDAN6:35;
  hence thesis by A1,A2,A3,CONNSP_2:3,TOPREAL6:15;
end;

theorem Th20:
  for x being Point of R^1, M being a_neighborhood of x ex N being
  Neighbourhood of x st N c= M
proof
  let x be Point of R^1, M be a_neighborhood of x;
  consider V being Subset of R^1 such that
A1: V is open and
A2: V c= M and
A3: x in V by CONNSP_2:6;
  consider r being Real such that
A4: r > 0 and
A5: ].x-r,x+r.[ c= V by A1,A3,FRECHET:8;
  reconsider N = ].x-r,x+r.[ as Neighbourhood of x by A4,RCOMP_1:def 6;
  take N;
  thus thesis by A2,A5;
end;

theorem Th21:
  for f being Function of R^1,R^1, g being PartFunc of REAL,REAL,
x being Point of R^1 st f = g & g is_continuous_in x holds f is_continuous_at x
proof
  let f be Function of R^1,R^1, g be PartFunc of REAL,REAL, x be Point of R^1
  such that
A1: f = g and
A2: g is_continuous_in x;
  let G be a_neighborhood of f.x;
  consider Z being Neighbourhood of g.x such that
A3: Z c= G by A1,Th20;
  consider N being Neighbourhood of x such that
A4: g.:N c= Z by A2,FCONT_1:5;
  reconsider H = N as a_neighborhood of x by Th19,TOPMETR:17;
  take H;
  thus thesis by A1,A3,A4;
end;

theorem
  for f being Function of R^1,R^1, g being Function of REAL,REAL st f =
  g & g is continuous holds f is continuous
proof
  let f be Function of R^1,R^1, g be Function of REAL,REAL such that
A1: f = g and
A2: g is continuous;
  for x being Point of R^1 holds f is_continuous_at x
  proof
    let x be Point of R^1;
    dom f = REAL by A1,FUNCT_2:def 1;
    then x in dom g by A1;
    then g is_continuous_in x by A2;
    hence thesis by A1,Th21;
  end;
  hence thesis by TMAP_1:44;
end;

theorem
  a <= r & s <= b implies [.r,s.] is closed Subset of
  Closed-Interval-TSpace(a,b)
proof
  set T = Closed-Interval-TSpace(a,b);
  set A = [.r,s.];
  assume that
A1: a <= r and
A2: s <= b;
  per cases;
  suppose
    r > s;
    then A = {}T by XXREAL_1:29;
    hence thesis;
  end;
  suppose
    r <= s;
    then a <= s by A1,XXREAL_0:2;
    then the carrier of T = [.a,b.] by A2,TOPMETR:18,XXREAL_0:2;
    then reconsider A as Subset of T by A1,A2,XXREAL_1:34;
    reconsider C = A as Subset of R^1 by TOPMETR:17;
    C is closed & C /\ [#]T = A by TREAL_1:1,XBOOLE_1:28;
    hence thesis by PRE_TOPC:13;
  end;
end;

theorem
  a <= r & s <= b implies ].r,s.[ is open Subset of Closed-Interval-TSpace(a,b)
proof
  set T = Closed-Interval-TSpace(a,b);
  set A = ].r,s.[;
  assume that
A1: a <= r and
A2: s <= b;
  per cases;
  suppose
    r >= s;
    then A = {}T by XXREAL_1:28;
    hence thesis;
  end;
  suppose
    r < s;
    then a < s by A1,XXREAL_0:2;
    then the carrier of T = [.a,b.] by A2,TOPMETR:18,XXREAL_0:2;
    then reconsider A as Subset of T by A1,A2,XXREAL_1:37;
    reconsider C = A as Subset of R^1 by TOPMETR:17;
    C is open & C /\ [#]T = A by JORDAN6:35,XBOOLE_1:28;
    hence thesis by TOPS_2:24;
  end;
end;

theorem
  a <= b & a <= r implies ].r,b.] is open Subset of Closed-Interval-TSpace(a,b)
proof
  set T = Closed-Interval-TSpace(a,b);
  assume that
A1: a <= b and
A2: a <= r;
A3: the carrier of T = [.a,b.] by A1,TOPMETR:18;
  then reconsider A = ].r,b.] as Subset of T by A2,XXREAL_1:36;
  reconsider C = ].r,b+1.[ as Subset of R^1 by TOPMETR:17;
A4: C /\ [#]T c= A
  proof
    let x be object;
    assume
A5: x in C /\ [#]T;
    then
A6: x in C by XBOOLE_0:def 4;
    then reconsider x as Real;
A7: r < x by A6,XXREAL_1:4;
    x <= b by A3,A5,XXREAL_1:1;
    hence thesis by A7;
  end;
  b+0 < b+1 by XREAL_1:6;
  then A c= C by XXREAL_1:49;
  then A c= C /\ [#]T by XBOOLE_1:19;
  then C is open & C /\ [#]T = A by A4,JORDAN6:35;
  hence thesis by TOPS_2:24;
end;

theorem
  a <= b & r <= b implies [.a,r.[ is open Subset of Closed-Interval-TSpace(a,b)
proof
  set T = Closed-Interval-TSpace(a,b);
  assume that
A1: a <= b and
A2: r <= b;
A3: the carrier of T = [.a,b.] by A1,TOPMETR:18;
  then reconsider A = [.a,r.[ as Subset of T by A2,XXREAL_1:35;
  reconsider C = ].a-1,r.[ as Subset of R^1 by TOPMETR:17;
A4: C /\ [#]T c= A
  proof
    let x be object;
    assume
A5: x in C /\ [#]T;
    then
A6: x in C by XBOOLE_0:def 4;
    then reconsider x as Real;
A7: x < r by A6,XXREAL_1:4;
    a <= x by A3,A5,XXREAL_1:1;
    hence thesis by A7;
  end;
  a-1 < a-0 by XREAL_1:15;
  then A c= C by XXREAL_1:48;
  then A c= C/\[#]T by XBOOLE_1:19;
  then C is open & C /\ [#]T = A by A4,JORDAN6:35;
  hence thesis by TOPS_2:24;
end;

theorem Th27:
  a <= b & r <= s implies the carrier of [:Closed-Interval-TSpace(
  a,b),Closed-Interval-TSpace(r,s):] = [: [.a,b.], [.r,s.] :]
proof
  set C1 = Closed-Interval-TSpace(a,b);
  set C2 = Closed-Interval-TSpace(r,s);
  assume a <= b & r <= s;
  then the carrier of C1 = [.a,b.] & the carrier of C2 = [.r,s.] by TOPMETR:18;
  hence thesis by BORSUK_1:def 2;
end;

begin :: TOP-REAL 2

theorem
  |[a,b]| = (1,2) --> (a,b) by Th4;

theorem
  |[a,b]|.1 = a & |[a,b]|.2 = b
proof
  thus |[a,b]|.1 = ((1,2) --> (a,b)).1 by Th4
    .= a by FUNCT_4:63;
  thus |[a,b]|.2 = ((1,2) --> (a,b)).2 by Th4
    .= b by FUNCT_4:63;
end;

theorem Th30:
  closed_inside_of_rectangle(a,b,r,s) = product ((1,2)-->([.a,b.], [.r,s.]))
proof
  set A = [.a,b.], B = [.r,s.];
  set f = (1,2)-->(A,B);
  set R = closed_inside_of_rectangle(a,b,r,s);
A1: R = {p where p is Point of TOP-REAL 2: a <= p`1 & p`1 <= b & r <= p`2 &
  p`2 <= s} by JGRAPH_6:def 2;
  thus R c= product f
  proof
    let x be object;
    assume x in R;
    then consider p being Point of TOP-REAL 2 such that
A2: x = p and
A3: a <= p`1 & p`1 <= b & r <= p`2 & p`2 <= s by A1;
    |[p`1,p`2]| = (1,2) --> (p`1,p`2) by Th4;
    then
A4: p = (1,2) --> (p`1,p`2) by EUCLID:53;
    p`1 in A & p`2 in B by A3;
    hence thesis by A2,A4,HILBERT3:11;
  end;
  let x be object;
  assume
A5: x in product f;
  then consider g being Function such that
A6: x = g and
A7: dom g = dom f and
  for y being object st y in dom f holds g.y in f.y by CARD_3:def 5;
A8: g.2 in B by A5,A6,Th3;
A9: g.1 in A by A5,A6,Th3;
  then reconsider g1 = g.1, g2 = g.2 as Real by A8;
A10: dom f = {1,2} by FUNCT_4:62;
  then reconsider g as FinSequence by A7,FINSEQ_1:2,def 2;
A11: len g = 2 by A7,A10,FINSEQ_1:2,def 3;
  |[g1,g2]| = (1,2) --> (g1,g2) by Th4;
  then reconsider g as Point of TOP-REAL 2 by A11,FINSEQ_1:44;
A12: r <= g`2 & g`2 <= s by A8,XXREAL_1:1;
  a <= g`1 & g`1 <= b by A9,XXREAL_1:1;
  hence thesis by A1,A6,A12;
end;

theorem Th31:
  a <= b & r <= s implies |[a,r]| in closed_inside_of_rectangle(a, b,r,s)
proof
  set o = |[a,r]|;
A1: closed_inside_of_rectangle(a,b,r,s) = {p where p is Point of TOP-REAL 2:
a <= p`1 & p`1 <= b & r <= p`2 & p`2 <= s} & o`1 = a by JGRAPH_6:def 2;
A2: o`2 = r;
  assume a <= b & r <= s;
  hence thesis by A1,A2;
end;

definition
  let a, b, c, d be Real;
  func Trectangle(a,b,c,d) -> SubSpace of TOP-REAL 2 equals
  (TOP-REAL 2) |
  closed_inside_of_rectangle(a,b,c,d);
  coherence;
end;

theorem Th32:
  a <= b & r <= s implies Trectangle(a,b,r,s) is non empty
proof
  assume a <= b & r <= s;
  then |[a,r]| in closed_inside_of_rectangle(a,b,r,s) by Th31;
  hence the carrier of Trectangle(a,b,r,s) is non empty;
end;

registration
  let a, c be non positive Real;
  let b, d be non negative Real;
  cluster Trectangle(a,b,c,d) -> non empty;
  coherence by Th32;
end;

definition
  func R2Homeomorphism -> Function of [:R^1,R^1:], TOP-REAL 2 means
  :Def2:
  for x, y being Real holds it. [x,y] = <*x,y*>;
  existence
  by BORSUK_6:20;
  uniqueness
  proof
    let f, g be Function of [:R^1,R^1:], TOP-REAL 2 such that
A1: for x, y being Real holds f. [x,y] = <*x,y*> and
A2: for x, y being Real holds g. [x,y] = <*x,y*>;
    let a be Point of [:R^1,R^1:];
    consider x, y being Element of R such that
A3: a = [x,y] by Lm1,DOMAIN_1:1;
    thus f.a = <*x,y*> by A1,A3
    .= g.a by A2,A3;
  end;
end;

theorem Th33:
  for A, B being Subset of REAL holds R2Homeomorphism.:[:A,B:] =
  product ((1,2) --> (A,B))
proof
  for x, y being Real holds R2Homeomorphism. [x,y] = <*x,y*> by Def2;
  hence thesis by TOPREAL6:75;
end;

theorem Th34:
  R2Homeomorphism is being_homeomorphism
proof
  for x, y being Real holds R2Homeomorphism. [x,y] = <*x,y*> by Def2;
  hence thesis by TOPREAL6:76;
end;

theorem Th35:
  a <= b & r <= s implies R2Homeomorphism | the carrier of [:
  Closed-Interval-TSpace(a,b),Closed-Interval-TSpace(r,s):] is Function of [:
Closed-Interval-TSpace(a,b),Closed-Interval-TSpace(r,s):], Trectangle(a,b,r,s)
proof
  set C1 = Closed-Interval-TSpace(a,b);
  set C2 = Closed-Interval-TSpace(r,s);
  set TR = Trectangle(a,b,r,s);
  set h = R2Homeomorphism | the carrier of [:C1,C2:];
  assume a <= b & r <= s;
  then
A1: the carrier of [:C1,C2:] = [: [.a,b.], [.r,s.] :] by Th27;
  dom R2Homeomorphism = [:R,R:] by Lm1,FUNCT_2:def 1;
  then
A2: dom h = the carrier of [:C1,C2:] by A1,RELAT_1:62,TOPMETR:17,ZFMISC_1:96;
  rng h c= the carrier of TR
  proof
    let y be object;
A3: the carrier of TR = closed_inside_of_rectangle(a,b,r,s) &
closed_inside_of_rectangle(a,b,r,s) = {p where p is Point of TOP-REAL 2: a <= p
    `1 & p`1 <= b & r <= p`2 & p`2 <= s} by JGRAPH_6:def 2,PRE_TOPC:8;
    assume y in rng h;
    then consider x being object such that
A4: x in dom h and
A5: h.x = y by FUNCT_1:def 3;
    reconsider x as Point of [:R^1,R^1:] by A4;
    dom h c= [:R,R:] by A1,A2,TOPMETR:17,ZFMISC_1:96;
    then consider x1, x2 being Element of R such that
A6: x = [x1,x2] by A4,DOMAIN_1:1;
A7: x2 in [.r,s.] by A1,A2,A4,A6,ZFMISC_1:87;
A8: h.x = R2Homeomorphism.x by A4,FUNCT_1:47;
    then reconsider p = h.x as Point of TOP-REAL 2;
A9: h.x = <*x1,x2*> by A8,A6,Def2;
    then x2 = p`2;
    then
A10: r <= p`2 & p`2 <= s by A7,XXREAL_1:1;
A11: x1 in [.a,b.] by A1,A2,A4,A6,ZFMISC_1:87;
    x1 = p`1 by A9;
    then a <= p`1 & p`1 <= b by A11,XXREAL_1:1;
    hence thesis by A5,A3,A10;
  end;
  hence thesis by A2,FUNCT_2:2;
end;

theorem Th36:
  a <= b & r <= s implies for h being Function of [:
Closed-Interval-TSpace(a,b),Closed-Interval-TSpace(r,s):], Trectangle(a,b,r,s)
  st h = R2Homeomorphism | the carrier of [:Closed-Interval-TSpace(a,b),
  Closed-Interval-TSpace(r,s):] holds h is being_homeomorphism
proof
  assume
A1: a <= b & r <= s;
  set TR = Trectangle(a,b,r,s);
A2: closed_inside_of_rectangle(a,b,r,s) = {p where p is Point of TOP-REAL 2:
  a <= p`1 & p`1 <= b & r <= p`2 & p`2 <= s} by JGRAPH_6:def 2;
  set p = |[a,r]|;
  p`1 = a & p`2 = r;
  then p in closed_inside_of_rectangle(a,b,r,s) by A1,A2;
  then reconsider T0 = TR as non empty SubSpace of TOP-REAL 2;
  set C2 = Closed-Interval-TSpace(r,s);
  set C1 = Closed-Interval-TSpace(a,b);
  let h be Function of [:C1,C2:], TR such that
A3: h = R2Homeomorphism | the carrier of [:C1,C2:];
  reconsider S0 = [:C1,C2:] as non empty SubSpace of [:R^1,R^1:] by BORSUK_3:21
;
  reconsider g = h as Function of S0,T0;
A4: the carrier of TR = closed_inside_of_rectangle(a,b,r,s) by PRE_TOPC:8;
A5: g is onto
  proof
    thus rng g c= the carrier of T0;
    let y be object;
A6: the carrier of [:C1,C2:] = [:[.a,b.],[.r,s.]:] & dom g = the carrier
    of S0 by A1,Th27,FUNCT_2:def 1;
    assume y in the carrier of T0;
    then consider p being Point of TOP-REAL 2 such that
A7: y = p and
A8: a <= p`1 & p`1 <= b & r <= p`2 & p`2 <= s by A2,A4;
    p`1 in [.a,b.] & p`2 in [.r,s.] by A8;
    then
A9: [p`1,p`2] in dom g by A6,ZFMISC_1:def 2;
    then g. [p`1,p`2] = R2Homeomorphism. [p`1,p`2] by A3,FUNCT_1:49
      .= |[p`1,p`2]| by Def2
      .= y by A7,EUCLID:53;
    hence thesis by A9,FUNCT_1:def 3;
  end;
  g = R2Homeomorphism|S0 by A3;
  hence thesis by A5,Th34,JORDAN16:9;
end;

theorem
  a <= b & r <= s implies [:Closed-Interval-TSpace(a,b),
  Closed-Interval-TSpace(r,s):], Trectangle(a,b,r,s) are_homeomorphic
proof
  set C1 = Closed-Interval-TSpace(a,b);
  set C2 = Closed-Interval-TSpace(r,s);
  assume
A1: a <= b & r <= s;
  then reconsider
  h = R2Homeomorphism | the carrier of [:C1,C2:] as Function of [:
  C1,C2:], Trectangle(a,b,r,s) by Th35;
  take h;
  thus thesis by A1,Th36;
end;

theorem Th38:
  a <= b & r <= s implies for A being Subset of
  Closed-Interval-TSpace(a,b), B being Subset of Closed-Interval-TSpace(r,s)
  holds product ((1,2)-->(A,B)) is Subset of Trectangle(a,b,r,s)
proof
  set T = Closed-Interval-TSpace(a,b);
  set S = Closed-Interval-TSpace(r,s);
  assume a <= b & r <= s;
  then
A1: the carrier of T = [.a,b.] & the carrier of S = [.r,s.] by TOPMETR:18;
  let A be Subset of T;
  let B be Subset of S;
  closed_inside_of_rectangle(a,b,r,s) = product ((1,2)-->([.a,b.],[.r,s.])
  ) by Th30;
  then product ((1,2)-->(A,B)) c= closed_inside_of_rectangle(a,b,r,s) by A1,
TOPREAL6:21;
  hence thesis by PRE_TOPC:8;
end;

theorem
  a <= b & r <= s implies for A being open Subset of
Closed-Interval-TSpace(a,b), B being open Subset of Closed-Interval-TSpace(r,s)
  holds product ((1,2)-->(A,B)) is open Subset of Trectangle(a,b,r,s)
proof
  set T = Closed-Interval-TSpace(a,b);
  set S = Closed-Interval-TSpace(r,s);
  assume
A1: a <= b & r <= s;
  then reconsider
  h = R2Homeomorphism | the carrier of [:Closed-Interval-TSpace(a,b
  ),Closed-Interval-TSpace(r,s):] as Function of [:Closed-Interval-TSpace(a,b),
  Closed-Interval-TSpace(r,s):], Trectangle(a,b,r,s) by Th35;
  let A be open Subset of T, B be open Subset of S;
  reconsider P = product ((1,2)-->(A,B)) as Subset of Trectangle(a,b,r,s) by A1
,Th38;
A2: [:A,B:] is open by BORSUK_1:6;
  the carrier of S is Subset of R^1 by TSEP_1:1;
  then
A3: B is Subset of REAL by TOPMETR:17,XBOOLE_1:1;
  the carrier of T is Subset of R^1 by TSEP_1:1;
  then
A4: A is Subset of REAL by TOPMETR:17,XBOOLE_1:1;
A5: h.:[:A,B:] = R2Homeomorphism.:[:A,B:] by RELAT_1:129
    .= P by A4,A3,Th33;
  h is being_homeomorphism & Trectangle(a,b,r,s) is non empty by A1,Th32,Th36;
  hence thesis by A5,A2,TOPGRP_1:25;
end;

theorem
  a <= b & r <= s implies for A being closed Subset of
Closed-Interval-TSpace(a,b), B being closed Subset of Closed-Interval-TSpace(r,
  s) holds product ((1,2)-->(A,B)) is closed Subset of Trectangle(a,b,r,s)
proof
  set T = Closed-Interval-TSpace(a,b);
  set S = Closed-Interval-TSpace(r,s);
  assume
A1: a <= b & r <= s;
  then reconsider
  h = R2Homeomorphism | the carrier of [:Closed-Interval-TSpace(a,b
  ),Closed-Interval-TSpace(r,s):] as Function of [:Closed-Interval-TSpace(a,b),
  Closed-Interval-TSpace(r,s):], Trectangle(a,b,r,s) by Th35;
  let A be closed Subset of T, B be closed Subset of S;
  reconsider P = product ((1,2)-->(A,B)) as Subset of Trectangle(a,b,r,s) by A1
,Th38;
A2: [:A,B:] is closed by TOPALG_3:15;
  the carrier of S is Subset of R^1 by TSEP_1:1;
  then
A3: B is Subset of REAL by TOPMETR:17,XBOOLE_1:1;
  the carrier of T is Subset of R^1 by TSEP_1:1;
  then
A4: A is Subset of REAL by TOPMETR:17,XBOOLE_1:1;
A5: h.:[:A,B:] = R2Homeomorphism.:[:A,B:] by RELAT_1:129
    .= P by A4,A3,Th33;
  h is being_homeomorphism & Trectangle(a,b,r,s) is non empty by A1,Th32,Th36;
  hence thesis by A5,A2,TOPS_2:58;
end;