:: The Definition of Topological Manifolds
::  by Marco Riccardi
::
:: Received August 17, 2010
:: Copyright (c) 2010 Association of Mizar Users

environ

 vocabularies NUMBERS, SUBSET_1, XREAL_0, ORDINAL1, PRE_TOPC, EUCLID, ARYTM_1,
      ARYTM_3, SUPINF_2, XBOOLE_0, FUNCOP_1, ORDINAL2, TOPS_1, RCOMP_1,
      XXREAL_0, METRIC_1, TARSKI, STRUCT_0, REAL_1, COMPLEX1, SETFAM_1,
      PCOMPS_1, TOPS_2, T_0TOPSP, CONNSP_2, FUNCT_1, RELAT_1, CARD_1, SQUARE_1,
      TOPMETR, MEMBERED, XXREAL_1, XXREAL_2, WAYBEL23, COMPTS_1, RLVECT_3,
      NATTRA_1, ZFMISC_1, FRECHET, CARD_3, MFOLD_1;
 notations TARSKI, XBOOLE_0, SUBSET_1, SETFAM_1, FUNCT_1, TOPS_2, RELAT_1,
      RELSET_1, PARTFUN1, FUNCT_2, ORDINAL1, NAT_1, NUMBERS, VALUED_0,
      VALUED_1, XCMPLX_0, XREAL_0, XXREAL_0, COMPLEX1, REAL_1, STRUCT_0,
      RVSUM_1, PRE_TOPC, METRIC_1, TOPREAL9, TOPS_1, ALGSTR_0, RLVECT_1,
      BORSUK_3, CONNSP_2, TSEP_1, METRIZTS, PCOMPS_1, COMPTS_1, EUCLID,
      SQUARE_1, TOPMETR, TMAP_1, XXREAL_1, MEMBERED, XXREAL_2, TOPREAL6,
      WAYBEL23, CANTOR_1, CARD_1, TDLAT_3, ZFMISC_1, CARD_3, YELLOW_8, FRECHET;
 constructors MONOID_0, TOPREAL9, TOPREALB, SQUARE_1, FUNCSDOM, TOPS_1, TSEP_1,
      BORSUK_3, METRIZTS, PCOMPS_1, RLVECT_1, COMPLEX1, COMPTS_1, XCMPLX_0,
      NAT_1, EUCLID, BINOP_2, TOPMETR, TMAP_1, MEMBERED, XXREAL_2, TOPREAL6,
      SEQ_1, WAYBEL23, CANTOR_1, TDLAT_3, FUNCT_2, YELLOW_8, FRECHET;
 registrations XBOOLE_0, XXREAL_0, XREAL_0, XCMPLX_0, SQUARE_1, NAT_1,
      MEMBERED, STRUCT_0, METRIC_1, MONOID_0, EUCLID, TOPALG_2, VALUED_0,
      FINSEQ_1, FUNCT_1, RELAT_1, PRE_TOPC, TOPS_1, CARD_1, TSEP_1, TOPREAL9,
      PCOMPS_1, RLVECT_1, COMPLEX1, TMAP_1, COMPTS_1, TOPMETR, XXREAL_2,
      TOPREAL6, SPPOL_1, WAYBEL23, METRIZTS, RLVECT_3, TOPREAL1, YELLOW13,
      YELLOW_8, KURATO_2, SUBSET_1;
 requirements NUMERALS, BOOLE, SUBSET, ARITHM, REAL;
 definitions TARSKI, XBOOLE_0, XREAL_0, XXREAL_2, XCMPLX_0, ALGSTR_0, STRUCT_0,
      RELAT_1, FUNCT_1, FUNCT_2, ORDINAL1, MEMBERED, PRE_TOPC, TOPS_2,
      T_0TOPSP, EUCLID, PCOMPS_1, TOPREAL9, SQUARE_1, ABSVALUE, TMAP_1,
      METRIZTS, FRECHET, YELLOW_8, WAYBEL23;
 theorems TOPRNS_1, XREAL_0, TARSKI, FUNCT_2, EUCLID, XBOOLE_1, FUNCOP_1,
      JORDAN2C, XCMPLX_1, ABSVALUE, XXREAL_1, XXREAL_2, GOBOARD6, XREAL_1,
      RLVECT_1, ORDINAL1, ZFMISC_1, SETFAM_1, PRE_TOPC, TOPS_1, CONNSP_2,
      METRIZTS, PCOMPS_1, T_0TOPSP, YELLOW14, TOPGRP_1, XBOOLE_0, TSEP_1,
      BORSUK_3, TOPREAL9, BORSUK_4, RELAT_1, FUNCT_1, TOPALG_1, TOPS_2,
      JGRAPH_1, RELSET_1, SQUARE_1, EUCLID_2, XXREAL_0, JGRAPH_2, TOPMETR,
      TOPREAL3, JORDAN6, GOBOARD9, RCOMP_1, JORDAN, WAYBEL23, YELLOW12,
      MEMBERED, JGRAPH_3, JGRAPH_5, TDLAT_3, FRECHET, CARD_3, YELLOW_8;
 schemes FUNCT_2, TREES_2;

begin :: Preliminaries

registration
  let x, y be set;
  cluster {[x,y]} -> one-to-one;
  correctness
  proof
    set f = {[x,y]};
    let x1, x2 be set;
    assume x1 in dom f & x2 in dom f & f.x1 = f.x2; then
A1: x1 in {x} & x2 in {x} by RELAT_1:23;
    hence x1 = x by TARSKI:def 1 .= x2 by A1,TARSKI:def 1;
  end;
end;

reserve n for natural number;

theorem Th1:
  for T being non empty TopSpace holds T , T | [#]T are_homeomorphic
proof
  let X be non empty TopSpace;
  set f = id X;
  A1: dom f = [#]X by RELAT_1:71;
  A2: [#](X | ([#]X))=the carrier of (the TopStruct of X) by TSEP_1:100
  .= [#]X;
  then A3: rng f = [#](X | ([#]X)) by RELAT_1:71;
  reconsider f as Function of X, X | ([#]X) by A2;
  for P being Subset of X st P is closed holds (f")"P is closed
  proof
    let P be Subset of X;
    assume P is closed; then
    ([#]X) \ P is open by PRE_TOPC:def 6; then
    A4: ([#]X) \ P in the topology of X by PRE_TOPC:def 5;
    A5: for x being set holds x in (f")"P iff x in P
    proof
      let x be set;
      hereby
        assume A6: x in (f")"P;
        x in f.:P by A6,A3,TOPS_2:67; then
        consider y be set such that
        A7: [y,x] in f & y in P by RELAT_1:def 13;
        thus x in P by A7,RELAT_1:def 10;
      end;
      assume A8: x in P; then
      [x,x] in id X by RELAT_1:def 10; then
      x in f.:P by A8,RELAT_1:def 13;
      hence x in (f")"P by A3,TOPS_2:67;
    end;
    A9: ([#]X) \ P = ([#] (X | ([#]X))) \ (f")"P by A2,A5,TARSKI:2;
    ([#]X)\P = ([#]X /\ [#]X)\P .= (([#]X)\P) /\ [#]X by XBOOLE_1:49; then
    ([#]X)\P in the topology of (X | ([#]X)) by A2,A4,PRE_TOPC:def 9; then
    ([#] (X | ([#]X))) \ (f")"P is open by A9,PRE_TOPC:def 5;
    hence (f")"P is closed by PRE_TOPC:def 6;
  end; then
A10: f" is continuous by PRE_TOPC:def 12;
  f is continuous by JGRAPH_1:63; then
  f is being_homeomorphism by A1,A3,A10,TOPS_2:def 5;
  hence thesis by T_0TOPSP:def 1;
end;

theorem Th2:
  for X being non empty SubSpace of TOP-REAL n, f being Function of X,R^1
  st f is continuous
  ex g being Function of X,TOP-REAL n st
  (for a being Point of X, b being Point of TOP-REAL n, r being real number
  st a = b & f.a = r holds g.b = r*b) & g is continuous
proof
  let X be non empty SubSpace of TOP-REAL n, f be Function of X,R^1;
  assume A1: f is continuous;
  defpred P[set,set] means
  for b being Point of TOP-REAL n, r being real number
  st $1 = b & f.$1 = r holds $2 = r*b;
  A2: for x being Element of X ex y being Point of TOP-REAL n st P[x,y]
  proof
    let x be Element of X;
    reconsider r = f.x as Real by TOPMETR:24;
    A3: x in the carrier of X;
    [#] X c= [#] TOP-REAL n by PRE_TOPC:def 9; then
    reconsider p = x as Point of TOP-REAL n by A3;
    set y = r*p;
    take y;
    thus P[x,y];
  end;
  ex g being Function of the carrier of X, the carrier of TOP-REAL n
  st for x being Element of X holds P[x,g.x] from FUNCT_2:sch 3(A2); then
  consider g be Function of X, TOP-REAL n such that
  A4: for x being Element of X holds for b being Point of TOP-REAL n,
  r being real number st x = b & f.x = r holds g.x = r*b;
  take g;
  for p being Point of X, V being Subset of TOP-REAL n
  st g.p in V & V is open holds
  ex W being Subset of X st p in W & W is open & g.:W c= V
  proof
    let p be Point of X, V be Subset of TOP-REAL n;
    A5: n in NAT by ORDINAL1:def 13;
    reconsider n1 = n as Element of NAT by ORDINAL1:def 13;
    reconsider gp = g.p as Point of Euclid n by TOPREAL3:13;
    A6: p in the carrier of X;
    [#] X c= [#] TOP-REAL n by PRE_TOPC:def 9; then
    reconsider pp = p as Point of TOP-REAL n1 by A6;
    reconsider fp = f.p as real number;
    assume g.p in V & V is open; then
    g.p in Int V by TOPS_1:55; then
    consider r0 be real number such that
    A7: r0 > 0 and
    A8: Ball(gp,r0) c= V by A5,GOBOARD6:8;
    per cases;
    suppose A9: fp = 0;
      reconsider W2 = Ball(pp, r0/2) /\ [#]X as Subset of X;
      Ball(pp, r0/2) in the topology of TOP-REAL n1
      by PRE_TOPC:def 5; then
      W2 in the topology of X by PRE_TOPC:def 9; then
      A10: W2 is open by PRE_TOPC:def 5;
      p in Ball(pp, r0/2) by A7,JORDAN:16; then
      A11: p in W2 by XBOOLE_0:def 4;
      set WW2 = {|.p2.| where p2 is Point of TOP-REAL n: p2 in W2};
      A12: |.pp.| in WW2 by A11;
      for x being set st x in WW2 holds x is real
      proof
        let x be set;
        assume x in WW2; then
        consider p2 be Point of TOP-REAL n1 such that
        A13: x = |.p2.| & p2 in W2;
        thus x is real by A13;
      end; then
      reconsider WW2 as non empty real-membered set by A12,MEMBERED:def 3;
      for x being ext-real number st x in WW2 holds
      x <= |.pp.|+r0/2
      proof
        let x be ext-real number;
        assume x in WW2; then
        consider p2 be Point of TOP-REAL n1 such that
        A14: x = |.p2.| & p2 in W2;
        p2 in Ball(pp, r0/2) by A14,XBOOLE_0:def 4; then
        A15: |. p2 - pp .| < r0/2 by TOPREAL9:7;
        |.p2.| - |. -pp .| <= |. p2 + -pp .| by TOPRNS_1:32; then
        |.p2.| - |. pp .| <= |. p2 + -pp .| by TOPRNS_1:27; then
        |.p2.| - |.pp.| <= r0/2 by A15,XXREAL_0:2; then
        |.p2.| - |.pp.| + |.pp.| <= r0/2 + |.pp.| by XREAL_1:8;
        hence x <= |.pp.|+r0/2 by A14;
      end; then
      |.pp.|+r0/2 is UpperBound of WW2 by XXREAL_2:def 1; then
      WW2 is bounded_above by XXREAL_2:def 10; then
      reconsider m = sup WW2 as real number;
      A16: m >= 0
      proof
        assume A17: m < 0;
        A18: m is UpperBound of WW2 by XXREAL_2:def 3;
        |.pp.| in WW2 by A11;
        hence contradiction by A17,A18,XXREAL_2:def 1;
      end;
      per cases by A16;
      suppose A19: m = 0;
        set G1 = REAL;
        REAL in the topology of R^1 by PRE_TOPC:def 1,TOPMETR:24; then
        reconsider G1 as open Subset of R^1 by PRE_TOPC:def 5;
        fp in G1 by XREAL_0:def 1; then
        consider W1 be Subset of X such that
        A20: p in W1 and
        A21: W1 is open and
        f.:W1 c= G1 by A1,JGRAPH_2:20;
        reconsider W3 = W1 /\ W2 as Subset of X;
        take W3;
        thus p in W3 by A20,A11,XBOOLE_0:def 4;
        thus W3 is open by A21,A10;
        g.:W3 c= Ball(gp,r0)
        proof
          let x be set;
          assume x in g.:W3; then
          consider q be set such that
          A22: q in dom g and
          A23: q in W3 and
          A24: g.q = x by FUNCT_1:def 12;
          reconsider q as Point of X by A22;
          A25: q in the carrier of X;
          [#] X c= [#] TOP-REAL n by PRE_TOPC:def 9; then
          reconsider qq = q as Point of TOP-REAL n1 by A25;
          reconsider fq = f.q as real number;
          A26: x = fq * qq by A4,A24; then
          reconsider gq = x as Point of Euclid n by TOPREAL3:13;
          reconsider gpp = gp as Point of TOP-REAL n1;
          reconsider gqq = gq as Point of TOP-REAL n1 by A26;
          A27: gpp = fp * pp by A4;
          reconsider r2 = fq-fp as Real by XREAL_0:def 1;
          A28: abs(fq-fp)*|.qq.| = abs(r2)*|.qq.| .= |.(fq-fp)*qq.|
          by TOPRNS_1:8;
          qq in W2 by A23,XBOOLE_0:def 4; then
          |.qq.| in WW2; then
          A29: |.qq.| <= m by XXREAL_2:4;
          A30:  gpp = 0.TOP-REAL n1 by A27,A9,EUCLID:33;
          |. gqq + -gpp .| <= |. gqq .| + |. -gpp .| by EUCLID_2:74; then
          |. gqq + -gpp .| <= |. gqq .| + |. 0.TOP-REAL n1 .|
          by JGRAPH_5:13,A30; then
          |. gqq + -gpp .| <= |. gqq .| + 0 by EUCLID_2:61; then
          |. gqq - gpp .| < r0 by A4,A24,A9,A29,A28,A7,A19; then
          gqq in Ball(gpp,r0);
          hence x in Ball(gp,r0) by TOPREAL9:13;
        end;
        hence thesis by A8,XBOOLE_1:1;
      end;
      suppose A31: m > 0;
        set G1 = ]. fp-r0/m, fp+r0/m .[;
        reconsider G1 as open Subset of R^1
        by JORDAN6:46,TOPMETR:24,XXREAL_1:225;
        A32: 0 + fp < r0/m + fp by A31,A7,XREAL_1:8;
        -r0/m + fp < 0 + fp by A31,A7,XREAL_1:8; then
        fp in G1 by A32,XXREAL_1:4; then
        consider W1 be Subset of X such that
        A33: p in W1 and
        A34: W1 is open and
        A35: f.:W1 c= G1 by A1,JGRAPH_2:20;
        reconsider W3 = W1 /\ W2 as Subset of X;
        take W3;
        thus p in W3 by A33,A11,XBOOLE_0:def 4;
        thus W3 is open by A34,A10;
        g.:W3 c= Ball(gp,r0)
        proof
          let x be set;
          assume x in g.:W3; then
          consider q be set such that
          A36: q in dom g and
          A37: q in W3 and
          A38: g.q = x by FUNCT_1:def 12;
          reconsider q as Point of X by A36;
          A39: q in the carrier of X;
          [#] X c= [#] TOP-REAL n by PRE_TOPC:def 9; then
          reconsider qq = q as Point of TOP-REAL n1 by A39;
          reconsider fq = f.q as real number;
          A40: x = fq * qq by A4,A38; then
          reconsider gq = x as Point of Euclid n by TOPREAL3:13;
          reconsider gpp = gp as Point of TOP-REAL n1;
          reconsider gqq = gq as Point of TOP-REAL n1 by A40;
          A41: gpp = fp * pp by A4;
          reconsider r2 = fq as Real by XREAL_0:def 1;
          A42: abs(fq)*|.qq.| = abs(r2)*|.qq.| .= |.fq*qq.|
          by TOPRNS_1:8;
          A43: q in dom f by A39,FUNCT_2:def 1;
          q in W1 by A37,XBOOLE_0:def 4; then
          f.q in f.:W1 by A43,FUNCT_1:def 12; then
          abs(fq-fp) < r0/m by A35,RCOMP_1:8; then
          abs(fq)*m < r0/m*m by A9,A31,XREAL_1:70; then
          abs(fq)*m < r0/(m/m) by XCMPLX_1:83; then
          A44: abs(fq)*m < r0/1 by A31,XCMPLX_1:60;
          qq in W2 by A37,XBOOLE_0:def 4; then
          |.qq.| in WW2; then
          |.qq.| <= m by XXREAL_2:4; then
          A45: |.qq.|*abs(fq) <= m*abs(fq) by XREAL_1:66;
          A46: gpp = 0.TOP-REAL n1 by A41,A9,EUCLID:33;
          A47: |. gqq  .| < r0 by A40,A45,A42,A44,XXREAL_0:2;
          |. gqq + -gpp .| <= |. gqq .| + |. -gpp .| by EUCLID_2:74; then
          |. gqq + -gpp .| <= |. gqq .| + |. 0.TOP-REAL n1 .|
          by JGRAPH_5:13,A46; then
          |. gqq + -gpp .| <= |. gqq .| + 0 by EUCLID_2:61; then
          |. gqq - gpp .| < r0 by A47,XXREAL_0:2; then
          gqq in Ball(gpp,r0);
          hence x in Ball(gp,r0) by TOPREAL9:13;
        end;
        hence thesis by A8,XBOOLE_1:1;
      end;
    end;
    suppose A48: fp <> 0;
      reconsider W2 = Ball(pp, r0/2/abs(fp)) /\ [#]X as Subset of X;
      Ball(pp, r0/2/abs(fp)) in the topology of TOP-REAL n1
      by PRE_TOPC:def 5; then
      W2 in the topology of X by PRE_TOPC:def 9; then
      A49: W2 is open by PRE_TOPC:def 5;
      p in Ball(pp, r0/2/abs(fp)) by JORDAN:16,A48,A7; then
      A50: p in W2 by XBOOLE_0:def 4;
      set WW2 = {|.p2.| where p2 is Point of TOP-REAL n: p2 in W2};
      A51: |.pp.| in WW2 by A50;
      for x being set st x in WW2 holds x is real
      proof
        let x be set;
        assume x in WW2; then
        consider p2 be Point of TOP-REAL n1 such that
        A52: x = |.p2.| & p2 in W2;
        thus x is real by A52;
      end; then
      reconsider WW2 as non empty real-membered set by A51,MEMBERED:def 3;
      for x being ext-real number st x in WW2 holds
      x <= |.pp.|+r0/2/abs(fp)
      proof
        let x be ext-real number;
        assume x in WW2; then
        consider p2 be Point of TOP-REAL n1 such that
        A53: x = |.p2.| & p2 in W2;
        p2 in Ball(pp, r0/2/abs(fp)) by A53,XBOOLE_0:def 4; then
        A54: |. p2 - pp .| < r0/2/abs(fp) by TOPREAL9:7;
        |.p2.| - |. -pp .| <= |. p2 + -pp .| by TOPRNS_1:32; then
        |.p2.| - |. pp .| <= |. p2 + -pp .| by TOPRNS_1:27; then
        |.p2.| - |.pp.| <= r0/2/abs(fp) by A54,XXREAL_0:2; then
        |.p2.| - |.pp.| + |.pp.| <= r0/2/abs(fp) + |.pp.| by XREAL_1:8;
        hence x <= |.pp.|+r0/2/abs(fp) by A53;
      end; then
      |.pp.|+r0/2/abs(fp) is UpperBound of WW2 by XXREAL_2:def 1; then
      WW2 is bounded_above by XXREAL_2:def 10; then
      reconsider m = sup WW2 as real number;
      A55: m >= 0
      proof
        assume A56: m < 0;
        A57: m is UpperBound of WW2 by XXREAL_2:def 3;
        |.pp.| in WW2 by A50;
        hence contradiction by A56,A57,XXREAL_2:def 1;
      end;
      per cases by A55;
      suppose A58: m = 0;
        set G1 = REAL;
        REAL in the topology of R^1 by PRE_TOPC:def 1,TOPMETR:24; then
        reconsider G1 as open Subset of R^1 by PRE_TOPC:def 5;
        fp in G1 by XREAL_0:def 1; then
        consider W1 be Subset of X such that
        A59: p in W1 and
        A60: W1 is open and
        f.:W1 c= G1 by A1,JGRAPH_2:20;
        reconsider W3 = W1 /\ W2 as Subset of X;
        take W3;
        thus p in W3 by A59,A50,XBOOLE_0:def 4;
        thus W3 is open by A60,A49;
        g.:W3 c= Ball(gp,r0)
        proof
          let x be set;
          assume x in g.:W3; then
          consider q be set such that
          A61: q in dom g and
          A62: q in W3 and
          A63: g.q = x by FUNCT_1:def 12;
          reconsider q as Point of X by A61;
          A64: q in the carrier of X;
          [#] X c= [#] TOP-REAL n by PRE_TOPC:def 9; then
          reconsider qq = q as Point of TOP-REAL n1 by A64;
          reconsider fq = f.q as real number;
          A65: x = fq * qq by A4,A63; then
          reconsider gq = x as Point of Euclid n by TOPREAL3:13;
          reconsider gpp = gp as Point of TOP-REAL n1;
          reconsider gqq = gq as Point of TOP-REAL n1 by A65;
          A66: gpp = fp * pp by A4;
          reconsider r2 = fq-fp as Real by XREAL_0:def 1;
          reconsider r3 = fp as Real by XREAL_0:def 1;
          A67: abs(fq-fp)*|.qq.| = abs(r2)*|.qq.| .= |.(fq-fp)*qq.|
          by TOPRNS_1:8;
          qq in W2 by A62,XBOOLE_0:def 4; then
          |.qq.| in WW2; then
          A68: |.qq.| <= m by XXREAL_2:4;
          A69: abs(fp)*|.qq-pp.| = abs(r3)*|.qq-pp.| .= |.fp*(qq-pp).|
          by TOPRNS_1:8;
          qq in W2 by A62,XBOOLE_0:def 4; then
          qq in Ball(pp, r0/2/abs(fp)) by XBOOLE_0:def 4; then
          |.qq-pp.| < r0/2/abs(fp) by TOPREAL9:7; then
          abs(fp)*|.qq-pp.| < abs(fp)*(r0/2/abs(fp)) by A48,XREAL_1:70; then
          abs(fp)*|.qq-pp.| < r0/2/(abs(fp)/abs(fp)) by XCMPLX_1:82; then
          A70: abs(fp)*|.qq-pp.| < r0/2/1 by A48,XCMPLX_1:60;
          A71: |.(fq-fp)*qq.| + |.fp*(qq-pp).| < r0/2+r0/2
          by A68,A70,A69,A67,A58,XREAL_1:10;
          |.(fq-fp)*qq + fp*(qq-pp).| <= |.(fq-fp)*qq.| + |.fp*(qq-pp).|
          by EUCLID_2:74; then
          A72: |.(fq-fp)*qq + fp*(qq-pp).| < r0 by A71,XXREAL_0:2;
          (fq-fp)*qq + fp*(qq-pp) = fq*qq -fp*qq + fp*(qq-pp) by EUCLID:54
          .= fq*qq -fp*qq + (fp*qq -fp*pp) by EUCLID:53
          .= fq*qq -fp*qq +fp*qq -fp*pp by EUCLID:49
          .= fq*qq - fp*pp by EUCLID:52; then
          gqq in Ball(gpp,r0) by A65,A72,A66;
          hence x in Ball(gp,r0) by TOPREAL9:13;
        end;
        hence thesis by A8,XBOOLE_1:1;
      end;
      suppose A73: m > 0;
        set G1 = ]. fp-r0/2/m, fp+r0/2/m .[;
        reconsider G1 as open Subset of R^1
        by JORDAN6:46,TOPMETR:24,XXREAL_1:225;
        A74: 0 + fp < r0/2/m + fp by A73,A7,XREAL_1:8;
        -r0/2/m + fp < 0 + fp by A73,A7,XREAL_1:8; then
        fp in G1 by A74,XXREAL_1:4; then
        consider W1 be Subset of X such that
        A75: p in W1 and
        A76: W1 is open and
        A77: f.:W1 c= G1 by A1,JGRAPH_2:20;
        reconsider W3 = W1 /\ W2 as Subset of X;
        take W3;
        thus p in W3 by A75,A50,XBOOLE_0:def 4;
        thus W3 is open by A76,A49;
        g.:W3 c= Ball(gp,r0)
        proof
          let x be set;
          assume x in g.:W3; then
          consider q be set such that
          A78: q in dom g and
          A79: q in W3 and
          A80: g.q = x by FUNCT_1:def 12;
          reconsider q as Point of X by A78;
          A81: q in the carrier of X;
          [#] X c= [#] TOP-REAL n by PRE_TOPC:def 9; then
          reconsider qq = q as Point of TOP-REAL n1 by A81;
          reconsider fq = f.q as real number;
          A82: x = fq * qq by A4,A80; then
          reconsider gq = x as Point of Euclid n by TOPREAL3:13;
          reconsider gpp = gp as Point of TOP-REAL n1;
          reconsider gqq = gq as Point of TOP-REAL n1 by A82;
          A83: gpp = fp * pp by A4;
          reconsider r2 = fq-fp as Real by XREAL_0:def 1;
          reconsider r3 = fp as Real by XREAL_0:def 1;
          A84: abs(fq-fp)*|.qq.| = abs(r2)*|.qq.|
          .= |.(fq-fp)*qq.| by TOPRNS_1:8;
          A85: q in dom f by A81,FUNCT_2:def 1;
          q in W1 by A79,XBOOLE_0:def 4; then
          f.q in f.:W1 by A85,FUNCT_1:def 12; then
          abs(fq-fp) < r0/2/m by A77,RCOMP_1:8; then
          abs(fq-fp)*m < r0/2/m*m by A73,XREAL_1:70; then
          abs(fq-fp)*m < r0/2/(m/m) by XCMPLX_1:83; then
          A86: abs(fq-fp)*m < r0/2/1 by A73,XCMPLX_1:60;
          qq in W2 by A79,XBOOLE_0:def 4; then
          |.qq.| in WW2; then
          |.qq.| <= m by XXREAL_2:4; then
          |.qq.|*abs(fq-fp) <= m*abs(fq-fp) by XREAL_1:66; then
          A87: |.(fq-fp)*qq.| < r0/2 by A84,A86,XXREAL_0:2;
          A88: abs(fp)*|.qq-pp.| = abs(r3)*|.qq-pp.| .= |.fp*(qq-pp).|
          by TOPRNS_1:8;
          qq in W2 by A79,XBOOLE_0:def 4; then
          qq in Ball(pp, r0/2/abs(fp)) by XBOOLE_0:def 4; then
          |.qq-pp.| < r0/2/abs(fp) by TOPREAL9:7; then
          abs(fp)*|.qq-pp.| < abs(fp)*(r0/2/abs(fp)) by A48,XREAL_1:70; then
          abs(fp)*|.qq-pp.| < r0/2/(abs(fp)/abs(fp)) by XCMPLX_1:82; then
          A89: abs(fp)*|.qq-pp.| < r0/2/1 by A48,XCMPLX_1:60;
          A90: |.(fq-fp)*qq.| + |.fp*(qq-pp).| < r0/2+r0/2
          by A87,A89,A88,XREAL_1:10;
          |.(fq-fp)*qq + fp*(qq-pp).| <= |.(fq-fp)*qq.| + |.fp*(qq-pp).|
          by EUCLID_2:74; then
          A91: |.(fq-fp)*qq + fp*(qq-pp).| < r0 by A90,XXREAL_0:2;
          (fq-fp)*qq + fp*(qq-pp) = fq*qq -fp*qq + fp*(qq-pp) by EUCLID:54
          .= fq*qq -fp*qq + (fp*qq -fp*pp) by EUCLID:53
          .= fq*qq -fp*qq +fp*qq -fp*pp by EUCLID:49
          .= fq*qq - fp*pp by EUCLID:52; then
          gqq in Ball(gpp,r0) by A82,A83,A91;
          hence x in Ball(gp,r0) by TOPREAL9:13;
        end;
        hence thesis by A8,XBOOLE_1:1;
      end;
    end;
  end;
  hence thesis by A4,JGRAPH_2:20;
end;

definition
  let n;
  let S be Subset of TOP-REAL n;
  attr S is ball means :Def1:
  ex p being Point of TOP-REAL n, r being real number st S = Ball(p,r);
end;

registration
  let n;
  cluster ball Subset of TOP-REAL n;
  correctness
  proof
    take Ball(the Point of TOP-REAL n,the real number);
    thus thesis by Def1;
  end;
  cluster ball -> open Subset of TOP-REAL n;
  correctness
  proof
    let S be Subset of TOP-REAL n;
    assume S is ball; then
    ex p be Point of TOP-REAL n, r be real number st S = Ball(p,r) by Def1;
    hence thesis;
  end;
end;

registration
  let n;
  cluster non empty ball Subset of TOP-REAL n;
  correctness
  proof
    reconsider S = Ball(0.(TOP-REAL n),1) as ball Subset of TOP-REAL n by Def1;
    take S;
    thus thesis;
  end;
end;

reserve p for Point of TOP-REAL n, r for real number;

theorem Th3:
  for S being open Subset of TOP-REAL n st p in S holds
  ex B being ball Subset of TOP-REAL n st B c= S & p in B
proof
  let S be open Subset of TOP-REAL n;
  assume A1: p in S;
  A2: TopStruct(# the carrier of TOP-REAL n,the topology of TOP-REAL n #)
  = TopSpaceMetr (Euclid n) by EUCLID:def 8;
  A3: S in Family_open_set Euclid n by A2,PRE_TOPC:def 5;
  reconsider x=p as Element of Euclid n by A2;
  consider r be Real such that
  A4: r > 0 & Ball(x,r) c= S by A1,A3,PCOMPS_1:def 5;
  reconsider r as positive (real number) by A4;
  reconsider n1 = n as Element of NAT by ORDINAL1:def 13;
  reconsider B = Ball(p,r) as ball Subset of TOP-REAL n by Def1;
  take B;
  reconsider p1=p as Point of TOP-REAL n1;
  Ball(x,r) =  Ball(p1,r) by TOPREAL9:13;
  hence thesis by A4,GOBOARD6:4;
end;

definition
  let n,p,r;
  func Tball(p,r) -> SubSpace of TOP-REAL n equals
  (TOP-REAL n) | Ball(p,r);
  correctness;
end;

definition
  let n;
  func Tunit_ball(n) -> SubSpace of TOP-REAL n equals
  Tball(0.(TOP-REAL n),1);
  correctness;
end;

registration
  let n;
  cluster Tunit_ball(n) -> non empty;
  correctness;
  let p;
  let s be positive (real number);
  cluster Tball(p,s) -> non empty;
  correctness;
end;

theorem Th4:
  the carrier of Tball(p,r) = Ball(p,r)
proof
  [#]Tball(p,r) = Ball(p,r) by PRE_TOPC:def 10;
  hence thesis;
end;

theorem Th5:
  n <> 0 & p is Point of Tunit_ball(n) implies |. p .| < 1
proof
  reconsider j = 1 as real number;
  assume n <> 0; then
  reconsider n1 = n as non empty Element of NAT by ORDINAL1:def 13;
  assume p is Point of Tunit_ball(n); then
  p in the carrier of Tball(0.(TOP-REAL n1),j);
  then p in Ball(0.(TOP-REAL n1),1) by Th4;
  hence thesis by TOPREAL9:10;
end;

theorem Th6:
  for f being Function of Tunit_ball n, TOP-REAL n st n <> 0 &
  for a being Point of Tunit_ball n, b being Point of TOP-REAL n
      st a = b holds f.a = 1/(1-|.b.|*|.b.|)*b
  holds f is being_homeomorphism
proof
  let f being Function of Tunit_ball n, TOP-REAL n such that
  A1: n <> 0 and
  A2: for a being Point of Tunit_ball n, b being Point of TOP-REAL n st
  a = b holds f.a = 1/(1-|.b.|*|.b.|)*b;
  A3: dom f = [#]Tunit_ball n by FUNCT_2:def 1;
  A4: [#] Tunit_ball n c= [#] TOP-REAL n by PRE_TOPC:def 9;
  reconsider n1 = n as non empty Element of NAT by A1,ORDINAL1:def 13;
  for y being set st y in [#]TOP-REAL n1 holds ex x being set st [x,y] in f
  proof
    let y be set;
    assume y in [#]TOP-REAL n1; then
    reconsider py = y as Point of TOP-REAL n1;
    per cases;
    suppose A5: |.py.| = 0;
      set x = py;
      |.x - 0.TOP-REAL n1.| < 1 by A5,RLVECT_1:26; then
      x in Ball(0.TOP-REAL n, 1); then
      A6: x in dom f by A3,Th4;
      take x;
      f.x = 1/(1-|.x.|*|.x.|)*x by A6,A2
      .= py by A5,EUCLID:33;
      hence [x,y] in f by A6,FUNCT_1:def 4;
    end;
    suppose A7: |.py.| <> 0;
      set p2 = |.py.|*|.py.|;
      set x = 2/(1+sqrt(1+4*p2))*py;
      reconsider r = 2/(1+sqrt(1+4*p2)) as Real;
      A8: sqrt(1+4*p2) >= 0 by SQUARE_1:def 4;
      A9: |.x.| = abs(r)*|.py.| by TOPRNS_1:8
      .= r*|.py.| by A8,ABSVALUE:def 1;
      |.x.| < 1
      proof
        |.py.|*4 + (1+4*p2) > 0 + (1+4*p2) by A7,XREAL_1:8; then
        sqrt((1+2*|.py.|)^2) > sqrt(1+4*p2) by SQUARE_1:95; then
        1+2*|.py.| > sqrt(1+4*p2) by SQUARE_1:89; then
        1+2*|.py.|-sqrt(1+4*p2) > sqrt(1+4*p2)-sqrt(1+4*p2) by XREAL_1:11; then
        1-sqrt(1+4*p2)+2*|.py.|-2*|.py.| > 0 - 2*|.py.| by XREAL_1:11; then
        (1-sqrt(1+4*p2))*1 > -2*|.py.|; then
        (1-sqrt(1+4*p2))*((1+sqrt(1+4*p2))/(1+sqrt(1+4*p2))) > -2*|.py.|
        by A8,XCMPLX_1:60; then
        (1-(sqrt(1+4*p2))^2)/(1+sqrt(1+4*p2)) > -2*|.py.|; then
        (1-(1+4*p2))/(1+sqrt(1+4*p2)) > -2*|.py.| by SQUARE_1:def 4; then
        -4*p2/(1+sqrt(1+4*p2)) > -2*|.py.|; then
        2*|.py.|*(2*|.py.|)/(1+sqrt(1+4*p2))
        < 2*|.py.| by XREAL_1:26; then
        (2*|.py.|)*((2*|.py.|)/(1+sqrt(1+4*p2)))/(2*|.py.|)
        < 2*|.py.|/(2*|.py.|) by A7,XREAL_1:76; then
        (2*|.py.|)*((2*|.py.|)/(1+sqrt(1+4*p2)))/(2*|.py.|) < 1
        by A7,XCMPLX_1:60; then
        ((2*|.py.|)/(1+sqrt(1+4*p2)))/((2*|.py.|)/(2*|.py.|)) < 1
        by XCMPLX_1:78; then
        ((2*|.py.|)/(1+sqrt(1+4*p2)))/1 < 1 by A7,XCMPLX_1:60;
        hence thesis by A9;
      end; then
      |.x - 0.TOP-REAL n1.| < 1 by RLVECT_1:26; then
      x in Ball(0.TOP-REAL n1, 1); then
      A10: x in dom f by A3,Th4;
      take x;
      A11: sqrt(1+4*p2)>=0 by SQUARE_1:def 4;
      A12: 1-sqrt(1+4*p2)<>0
      proof
        assume 1-sqrt(1+4*p2)=0; then
        (sqrt(1+4*p2))^2 = 1; then
        1+4*p2 = 1 by SQUARE_1:def 4;
        hence contradiction by A7;
      end;
      |.x.|*|.x.| = (2/(1+sqrt(1+4*p2)))*(2/(1+sqrt(1+4*p2)))*p2 by A9
      .= (2*2)/((1+sqrt(1+4*p2))*(1+sqrt(1+4*p2)))*p2 by XCMPLX_1:77
      .= 4/(1+2*sqrt(1+4*p2)+(sqrt(1+4*p2))^2)*p2
      .= 4/(1+2*sqrt(1+4*p2)+(1+4*p2))*p2 by SQUARE_1:def 4
      .= 4/(2*(1+sqrt(1+4*p2)+2*p2))*p2
      .= 4/2/(1+sqrt(1+4*p2)+2*p2)*p2 by XCMPLX_1:79
      .= (2*p2)/(1+2*p2+sqrt(1+4*p2)); then
      A13: 1-|.x.|*|.x.| = (1+2*p2+sqrt(1+4*p2))/(1+2*p2+sqrt(1+4*p2))
      + -(2*p2)/(1+2*p2+sqrt(1+4*p2)) by A11,XCMPLX_1:60
      .= (1+sqrt(1+4*p2))/(1+2*p2+sqrt(1+4*p2))*1
      .= ((1+sqrt(1+4*p2))/(1+2*p2+sqrt(1+4*p2)))*
      ((1-sqrt(1+4*p2))/(1-sqrt(1+4*p2))) by A12,XCMPLX_1:60
      .= ((1+sqrt(1+4*p2))*(1-sqrt(1+4*p2)))/
      ((1-sqrt(1+4*p2))*(1+2*p2+sqrt(1+4*p2))) by XCMPLX_1:77
      .= (1-(sqrt(1+4*p2))^2)/
      (1+2*p2-2*p2*sqrt(1+4*p2)-sqrt(1+4*p2)*sqrt(1+4*p2))
      .= (1-(1+4*p2))/
      (1+2*p2-2*p2*sqrt(1+4*p2)-(sqrt(1+4*p2))^2) by SQUARE_1:def 4
      .= (-4*p2)/(1+2*p2-2*p2*sqrt(1+4*p2)-(1+4*p2)) by SQUARE_1:def 4
      .= (-4*p2)/((-2*p2)*(1+sqrt(1+4*p2)))
      .= 2*(-2*p2)/(-2*p2)/(1+sqrt(1+4*p2)) by XCMPLX_1:79
      .= 2*((-2*p2)/(-2*p2))/(1+sqrt(1+4*p2))
      .= 2*1/(1+sqrt(1+4*p2)) by A7,XCMPLX_1:60
      .= 2/(1+sqrt(1+4*p2));
      f.x = 1/(1-|.x.|*|.x.|)*x by A2,A10
      .= (r/r)*py by A13,EUCLID:34
      .= 1*py by A8,XCMPLX_1:60
      .= py by EUCLID:33;
      hence [x,y] in f by A10,FUNCT_1:def 4;
    end;
  end; then
  A14: rng f = [#]TOP-REAL n1 by RELSET_1:23;
  for x1,x2 being set st x1 in dom f & x2 in dom f & f.x1 = f.x2 holds
  x1 = x2
  proof
    let x1,x2 be set;
    A15: [#]Tunit_ball n c= [#] TOP-REAL n by PRE_TOPC:def 9;
    assume A16: x1 in dom f; then
    x1 in the carrier of Tunit_ball n; then
    reconsider px1 = x1 as Point of TOP-REAL n1 by A15;
    assume A17: x2 in dom f; then
    A18: x2 in the carrier of Tunit_ball n; then
    reconsider px2 = x2 as Point of TOP-REAL n1 by A15;
    assume A19: f.x1 = f.x2;
    A20: 1/(1-|.px1.|*|.px1.|)*px1 = f.x2 by A19,A16,A2
    .= 1/(1-|.px2.|*|.px2.|)*px2 by A17,A2;
    per cases;
    suppose A21: |.px1.| = 0; then
      A22: px1 = 0.TOP-REAL n by EUCLID_2:64;
      per cases by A22,EUCLID:35,A20,EUCLID:32;
      suppose 1/(1-|.px2.|*|.px2.|) = 0; then
        1-|.px2.|*|.px2.| = 0; then
        sqrt(|.px2.|^2) = 1 by SQUARE_1:83; then
        A23: |.px2.| = 1 by SQUARE_1:89;
        px2 in Ball(0.TOP-REAL n, 1) by A18,Th4; then
        consider p2 be Point of TOP-REAL n such that
        A24: p2=px2 & |.p2 - 0.TOP-REAL n.| < 1;
        thus thesis by A23,A24,RLVECT_1:26;
      end;
      suppose px2 = 0.TOP-REAL n; hence thesis by A21,EUCLID_2:64; end;
    end;
    suppose A25: |.px1.| <> 0; then
      |.px1.|*|.px1.| < 1*|.px1.| by A16,Th5,XREAL_1:70; then
      |.px1.|*|.px1.| < 1 by A16,Th5,XXREAL_0:2; then
      -|.px1.|*|.px1.| > -1 by XREAL_1:26; then
      A26: -|.px1.|*|.px1.| +1 > -1+1 by XREAL_1:8;
      A27: px1 = 1*px1 by EUCLID:33
      .= (1-|.px1.|*|.px1.|)/(1-|.px1.|*|.px1.|)*px1 by A26,XCMPLX_1:60
      .= (1-|.px1.|*|.px1.|)*((1/(1-|.px1.|*|.px1.|))*px1) by EUCLID:34
      .= (1-|.px1.|*|.px1.|)/(1-|.px2.|*|.px2.|)*px2 by A20,EUCLID:34;
      A28: px2 <> 0.TOP-REAL n1
      proof
        assume px2 = 0.TOP-REAL n1; then
        px1 = 0.TOP-REAL n1 by A27,EUCLID:32;
        hence contradiction by A25,TOPRNS_1:24;
      end; then
      A29: |.px2.| <> 0 by EUCLID_2:64;
      px2 in Ball(0.TOP-REAL n, 1) by A18,Th4; then
      consider p2 be Point of TOP-REAL n such that
      A30: p2=px2 & |.p2 - 0.TOP-REAL n.| < 1;
      A31: |.px2.| < 1 by A30,RLVECT_1:26; then
      |.px2.|*|.px2.| < 1*|.px2.| by A29,XREAL_1:70; then
      |.px2.|*|.px2.| < 1 by A31,XXREAL_0:2; then
      -|.px2.|*|.px2.| > -1 by XREAL_1:26; then
      A32: -|.px2.|*|.px2.| +1 > -1+1 by XREAL_1:8;
      set l = (1-|.px1.|*|.px1.|)/(1-|.px2.|*|.px2.|);
      1/(1-|.px2.|*|.px2.|)*px2
      = 1/(1-|.px1.|*|.px1.|)*l*px2 by A27,A20,EUCLID:34; then
      1/(1-|.px2.|*|.px2.|)*px2 -1/(1-|.px1.|*|.px1.|)*l*px2
      = 0.TOP-REAL n by EUCLID:40; then
      1/(1-|.px2.|*|.px2.|)*px2 + (-1/(1-|.px1.|*|.px1.|)*l)*px2
      = 0.TOP-REAL n by EUCLID:44; then
      A33: (1/(1-|.px2.|*|.px2.|)+ (-1/(1-|.px1.|*|.px1.|)*l))*px2
      = 0.TOP-REAL n by EUCLID:37;
      A34: l*l = abs(l)*abs(l)
      proof
        per cases by ABSVALUE:1;
        suppose abs l = l; hence thesis; end;
        suppose abs l = -l; hence thesis; end;
      end;
      1/(1-|.px2.|*|.px2.|)+ -1/(1-|.px1.|*|.px1.|)*l = 0
      by A28,A33,EUCLID:35; then
      1/(1-|.px2.|*|.px2.|) = 1*l/(1-|.px1.|*|.px1.|)
      .= 1/((1-|.px1.|*|.px1.|)/l) by XCMPLX_1:78; then
      1-|.px2.|*|.px2.| = (1-|.px1.|*|.px1.|)/l by XCMPLX_1:59; then
      l*(1-|.px2.|*|.px2.|)
      = (1-|.px1.|*|.px1.|)/(l/l) by XCMPLX_1:82
      .= (1-|.px1.|*|.px1.|)/1 by A26,A32,XCMPLX_1:60
      .= 1-(abs(l)*|.px2.|)*|.l*px2.| by A27,TOPRNS_1:8
      .= 1-(abs(l)*|.px2.|)*(abs(l)*|.px2.|) by TOPRNS_1:8
      .= 1-abs(l)*abs(l)*|.px2.|*|.px2.|
      .= 1-l*l*|.px2.|*|.px2.| by A34; then
      (1+l*|.px2.|*|.px2.|)*(1-l) = 0; then
      1-l = 0 by A26,A32;
      hence x1 = x2 by A27,EUCLID:33;
    end;
  end; then
  A35: f is one-to-one by FUNCT_1:def 8;
  consider f0 be Function of TOP-REAL n1, R^1 such that
  A36: (for p being Point of TOP-REAL n1 holds f0.p=1) & f0 is continuous
  by JGRAPH_2:30;
  consider f1 be Function of TOP-REAL n1, R^1 such that
  A37: (for p being Point of TOP-REAL n1 holds f1.p = |.p.|)
  & f1 is continuous by JORDAN2C:92;
  consider f2 be Function of TOP-REAL n,R^1 such that
  A38: (for p being Point of TOP-REAL n, r1 being real number
  st f1.p=r1 holds f2.p=r1*r1) & f2 is continuous by A37,JGRAPH_2:32;
  consider f3 be Function of TOP-REAL n,R^1 such that
  A39: (for p being Point of TOP-REAL n,r1,r2 being real number
  st f0.p=r1 & f2.p=r2 holds f3.p=r1-r2) & f3 is continuous
  by A36,A38,JGRAPH_2:31;
  reconsider f3 as continuous Function of TOP-REAL n,R^1 by A39;
  A40: for p being Point of TOP-REAL n holds f3.p = 1 - |.p.|*|.p.|
  proof
    let p be Point of TOP-REAL n;
    thus f3.p = f0.p - f2.p by A39 .= 1 - f2.p by A36
    .= 1 - f1.p*f1.p by A38 .= 1 - |.p.|*f1.p by A37
    .= 1 - |.p.|*|.p.| by A37;
  end;
  set f4 = f3|Tunit_ball n;
  for p being Point of Tunit_ball n holds f4.p <> 0
  proof
    let p be Point of Tunit_ball n;
    assume f4.p = 0; then
    A41: f3.p = 0 by FUNCT_1:72;
    p in the carrier of Tunit_ball n; then
    reconsider p1 = p as Point of TOP-REAL n1 by A4;
    A42: 1 - |.p1.|*|.p1.| = 0 by A41,A40;
    per cases;
    suppose |.p1.| = 0; hence contradiction by A42; end;
    suppose |.p1.| <> 0; then
      |.p1.|*|.p1.| < 1*|.p1.| by Th5,XREAL_1:70;
      hence contradiction by A42,Th5;
    end;
  end; then
  consider f5 be Function of Tunit_ball n,R^1 such that
  A43: (for p being Point of Tunit_ball n,r1 being real number st f4.p=r1
  holds f5.p=1/r1) & f5 is continuous by JGRAPH_2:36;
  consider f6 be Function of Tunit_ball n,TOP-REAL n such that
  A44: (for a being Point of Tunit_ball n, b being Point of TOP-REAL n,
  r being real number st a = b & f5.a = r holds f6.b = r*b) &
  f6 is continuous by A43,Th2;
  A45: dom f = the carrier of Tunit_ball(n) by FUNCT_2:def 1
  .= dom f6 by FUNCT_2:def 1;
  for x being set st x in dom f holds f.x = f6.x
  proof
    let x be set;
    assume A46: x in dom f; then
    A47: x in the carrier of Tunit_ball n;
    reconsider p1 = x as Point of Tunit_ball n by A46;
    reconsider p = x as Point of TOP-REAL n by A47,A4;
    f4.p = f3.p by A46,FUNCT_1:72
    .= 1 - |.p.|*|.p.| by A40; then
    f5.p1 = 1/(1 - |.p.|*|.p.|) by A43; then
    f6.p1 = 1/(1 - |.p.|*|.p.|)*p by A44;
    hence f.x = f6.x by A2;
  end; then
  A48: f = f6 by A45,FUNCT_1:9;
  consider f8 be Function of TOP-REAL n,R^1 such that
  A49: (for p being Point of TOP-REAL n,r1 being real number
  st f2.p=r1 holds f8.p=4*r1) & f8 is continuous
  by A38,JGRAPH_2:33;
  consider f9 be Function of TOP-REAL n,R^1 such that
  A50: (for p being Point of TOP-REAL n,r1,r2 being real number
  st f0.p=r1 & f8.p=r2 holds f9.p=r1+r2) & f9 is continuous
  by A49,A36,JGRAPH_2:29;
  A51: for p being Point of TOP-REAL n holds f9.p = 1 + 4*|.p.|*|.p.|
  proof
    let p be Point of TOP-REAL n;
    thus f9.p = f0.p + f8.p by A50 .= 1 + f8.p by A36 .= 1 + 4*f2.p by A49
    .= 1 + 4*(f1.p*f1.p) by A38 .= 1 + 4*(f1.p*|.p.|) by A37
    .= 1 + 4*(|.p.|*|.p.|) by A37 .= 1 + 4*|.p.|*|.p.|;
  end;
  A52: for p being Point of TOP-REAL n ex r being real number st f9.p=r & r>=0
  proof
    let p be Point of TOP-REAL n;
    set r = 1 + 4*|.p.|*|.p.|;
    take r;
    thus thesis by A51;
  end;
  consider f10 be Function of TOP-REAL n,R^1 such that
  A53: (for p being Point of TOP-REAL n,r1 being real number
  st f9.p=r1 holds f10.p=sqrt(r1)) & f10 is continuous
  by A52,A50,JGRAPH_3:15;
  consider f11 be Function of TOP-REAL n,R^1 such that
  A54: (for p being Point of TOP-REAL n,r1,r2 being real number
  st f0.p=r1 & f10.p=r2 holds f11.p=r1+r2) & f11 is continuous
  by A53,A36,JGRAPH_2:29;
  for p being Point of TOP-REAL n holds f11.p <> 0
  proof
    let p be Point of TOP-REAL n;
    A55: f11.p = f0.p + f10.p by A54 .= 1 + f10.p by A36
    .= 1 + sqrt(f9.p) by A53;
    consider r be real number such that
    A56: r = f9.p & r >= 0 by A52;
    sqrt(f9.p) >= 0 by A56,SQUARE_1:def 4;
    hence thesis by A55;
  end; then
  consider f12 be Function of TOP-REAL n,R^1 such that
  A57: (for p being Point of TOP-REAL n,r1 being real number st f11.p=r1
  holds f12.p=1/r1) & f12 is continuous by A54,JGRAPH_2:36;
  consider f13 be Function of TOP-REAL n,R^1 such that
  A58: (for p being Point of TOP-REAL n,r1 being real number
  st f12.p=r1 holds f13.p=2*r1) & f13 is continuous
  by A57,JGRAPH_2:33;
  A59: for p being Point of TOP-REAL n holds
  f13.p = 2/(1+sqrt(1 + 4*|.p.|*|.p.|))
  proof
    let p be Point of TOP-REAL n;
    thus f13.p = 2*f12.p by A58 .= 2*(1/f11.p) by A57
    .= 2/(f0.p+f10.p) by A54
    .= 2/(f0.p+sqrt(f9.p)) by A53
    .= 2/(1+sqrt(f9.p)) by A36
    .= 2/(1+sqrt(1 + 4*|.p.|*|.p.|)) by A51;
  end;
  reconsider X = TOP-REAL n as non empty SubSpace of TOP-REAL n by TSEP_1:2;
  consider f14 be Function of X, TOP-REAL n such that
  A60: (for a being Point of X, b being Point of TOP-REAL n,
  r being real number st a = b & f13.a = r holds f14.b = r*b) &
  f14 is continuous by A58,Th2;
  reconsider f14 as continuous Function of TOP-REAL n, TOP-REAL n by A60;
  A61: dom f14 = the carrier of TOP-REAL n by FUNCT_2:def 1;
  A62: for r being real number holds abs(r)*abs(r) = r*r
  proof
    let r be real number;
    per cases by ABSVALUE:1;
    suppose abs r = r; hence thesis; end;
    suppose abs r = -r; hence thesis; end;
  end;
  for y being set holds y in the carrier of Tunit_ball(n)
  iff ex x being set st x in dom f14 & y = f14.x
  proof
    let y be set;
    hereby
      assume A63: y in the carrier of Tunit_ball(n);
      [#] Tunit_ball(n) c= [#] TOP-REAL n by PRE_TOPC:def 9; then
      reconsider q = y as Point of TOP-REAL n1 by A63;
      |.q.| < 1 by A63,Th5; then
      |.q.|*|.q.| <= 1*|.q.| by XREAL_1:66; then
      |.q.|*|.q.| < 1 by A63,Th5,XXREAL_0:2; then
      A64: 0 < 1 - |.q.|*|.q.| by XREAL_1:52;
      set p = 1/(1-|.q.|*|.q.|)*q;
      |.p.| = abs(1/(1-|.q.|*|.q.|))*|.q.| by TOPRNS_1:8; then
      |.p.|*|.p.| = abs(1/(1-|.q.|*|.q.|))*abs(1/(1-|.q.|*|.q.|))*|.q.|*|.q.|
      .= (1/(1-|.q.|*|.q.|))*(1/(1-|.q.|*|.q.|))*|.q.|*|.q.| by A62
      .= (1*1)/((1-|.q.|*|.q.|)*(1-|.q.|*|.q.|))*|.q.|*|.q.| by XCMPLX_1:77
      .= |.q.|*|.q.|/((1-|.q.|*|.q.|)*(1-|.q.|*|.q.|)); then
      A65: 1 + 4*|.p.|*|.p.|
      = ((1-|.q.|*|.q.|)*(1-|.q.|*|.q.|))/((1-|.q.|*|.q.|)*(1-|.q.|*|.q.|))
      + 4*|.q.|*|.q.|/((1-|.q.|*|.q.|)*(1-|.q.|*|.q.|)) by A64,XCMPLX_1:60
      .= ((1+|.q.|*|.q.|)*(1+|.q.|*|.q.|))/((1-|.q.|*|.q.|)*(1-|.q.|*|.q.|))
      .= ((1+|.q.|*|.q.|)/(1-|.q.|*|.q.|))^2 by XCMPLX_1:77;
      sqrt(1 + 4*|.p.|*|.p.|) = (1+|.q.|*|.q.|)/(1-|.q.|*|.q.|)
      by A64,A65,SQUARE_1:89; then
      A66: 1+sqrt(1 + 4*|.p.|*|.p.|)
      = (1-|.q.|*|.q.|)/(1-|.q.|*|.q.|)+(1+|.q.|*|.q.|)/(1-|.q.|*|.q.|)
      by A64,XCMPLX_1:60
      .= 2/(1-|.q.|*|.q.|);
      reconsider x = p as set;
      take x;
      thus x in dom f14 by A61;
      thus f14.x = f13.p * p by A60
      .= 2/(2/(1-|.q.|*|.q.|)) * p by A66,A59
      .= (1-|.q.|*|.q.|) * p by XCMPLX_1:52
      .= (1-|.q.|*|.q.|)/(1-|.q.|*|.q.|) * q by EUCLID:34
      .= 1 * q by A64,XCMPLX_1:60
      .= y by EUCLID:33;
    end;
    given x be set such that
    A67: x in dom f14 & y = f14.x;
    reconsider p = x as Point of TOP-REAL n1 by A67;
    y in rng f14 by A67,FUNCT_1:12; then
    reconsider q = y as Point of TOP-REAL n1;
    y = (f13.p)*p by A60,A67
    .= 2/(1+sqrt(1 + 4*|.p.|*|.p.|))*p by A59; then
    |.q.| = abs(2/(1+sqrt(1 + 4*|.p.|*|.p.|)))*|.p.| by TOPRNS_1:8; then
    A68: |.q.|*|.q.| = abs(2/(1+sqrt(1 + 4*|.p.|*|.p.|)))*
    abs(2/(1+sqrt(1 + 4*|.p.|*|.p.|)))*|.p.|*|.p.|
    .= (2/(1+sqrt(1 + 4*|.p.|*|.p.|)))*(2/(1+sqrt(1 + 4*|.p.|*|.p.|)))*
    |.p.|*|.p.| by A62;
    |.q.|*|.q.| < 1
    proof
      assume |.q.|*|.q.| >= 1; then
      A69: ((2*2)/((1+sqrt(1 + 4*|.p.|*|.p.|))*(1+sqrt(1 + 4*|.p.|*|.p.|))))*
      |.p.|*|.p.| >= 1 by A68,XCMPLX_1:77;
      0 <= sqrt(1 + 4*|.p.|*|.p.|) by SQUARE_1:def 4; then
      4/(1+sqrt(1 + 4*|.p.|*|.p.|))^2*|.p.|*|.p.|*(1+sqrt(1 + 4*|.p.|*|.p.|))^2
      >= 1*(1+sqrt(1 + 4*|.p.|*|.p.|))^2
      by A69,XREAL_1:66; then
      (1+sqrt(1 + 4*|.p.|*|.p.|))^2/(1+sqrt(1 + 4*|.p.|*|.p.|))^2*4*|.p.|*|.p.|
      >= (1+sqrt(1 + 4*|.p.|*|.p.|))^2; then
      1*4*|.p.|*|.p.| >= (1+sqrt(1 + 4*|.p.|*|.p.|))^2 by XCMPLX_1:60; then
      4*|.p.|*|.p.| >= 1+2*sqrt(1 + 4*|.p.|*|.p.|)+
      (sqrt(1 + 4*|.p.|*|.p.|))^2; then
      4*|.p.|*|.p.| >= 1+2*sqrt(1 + 4*|.p.|*|.p.|)+(1+4*|.p.|*|.p.|)
      by SQUARE_1:def 4; then
      4*|.p.|*|.p.|-4*|.p.|*|.p.| >= 2+2*sqrt(1 + 4*|.p.|*|.p.|)+4*|.p.|*|.p.|
      -4*|.p.|*|.p.| by XREAL_1:11; then
      0/2 > 2*sqrt(1 + 4*|.p.|*|.p.|)/2;
      hence contradiction by SQUARE_1:def 4;
    end; then
    |.q.|^2 < 1; then
    A70: |.q.| < 1 by SQUARE_1:122;
    |. q + -0.TOP-REAL n1 .|<=|.q.| + |. -0.TOP-REAL n1 .| by EUCLID_2:74; then
    |. q + -0.TOP-REAL n1 .|<=|.q.| + |. 0.TOP-REAL n1 .| by JGRAPH_5:13; then
    |. q + -0.TOP-REAL n1 .|<=|.q.| + 0 by EUCLID_2:61; then
    |. q - 0.TOP-REAL n1 .| < 1 by A70,XXREAL_0:2; then
    q in Ball(0.TOP-REAL n1,1); then
    y in [#]Tball(0.TOP-REAL n,1) by PRE_TOPC:def 10;
    hence y in the carrier of Tunit_ball(n);
  end; then
  A71: rng f14 = the carrier of Tunit_ball n by FUNCT_1:def 5; then
  reconsider f14 as Function of TOP-REAL n, Tunit_ball n by A61,FUNCT_2:3;
  A72: dom f14 = the carrier of TOP-REAL n by FUNCT_2:def 1
  .= dom(f") by FUNCT_2:def 1;
  for x being set st x in dom f14 holds f14.x = f".x
  proof
    let x be set;
    assume A73: x in dom f14;
    reconsider g = f as Function;
    A74: f" = g" by A14,A35,TOPS_2:def 4;
    A75: f14.x in rng f14 by A73,FUNCT_1:12; then
    A76: f14.x in dom f by A71,FUNCT_2:def 1;
    reconsider p = x as Point of TOP-REAL n1 by A73;
    A77: f14.p = f13.p * p by A60 .= 2/(1+sqrt(1 + 4*|.p.|*|.p.|))*p by A59;
    reconsider y = f14.x as Point of Tunit_ball(n) by A75;
    f14.x in [#]Tunit_ball(n) by A75; then
    reconsider q = y as Point of TOP-REAL n1 by A4;
    A78: 0 <= sqrt(1 + 4*|.p.|*|.p.|) by SQUARE_1:def 4;
    |.q.| = abs(2/(1+sqrt(1 + 4*|.p.|*|.p.|)))*|.p.| by A77,TOPRNS_1:8; then
    |.q.|*|.q.| = abs(2/(1+sqrt(1 + 4*|.p.|*|.p.|)))*
    abs(2/(1+sqrt(1 + 4*|.p.|*|.p.|)))*|.p.|*|.p.|
    .= (2/(1+sqrt(1 + 4*|.p.|*|.p.|)))*(2/(1+sqrt(1 + 4*|.p.|*|.p.|)))*
    |.p.|*|.p.| by A62
    .= (2*2)/((1+sqrt(1 + 4*|.p.|*|.p.|))*(1+sqrt(1 + 4*|.p.|*|.p.|)))*
    |.p.|*|.p.| by XCMPLX_1:77
    .= 4*|.p.|*|.p.|/(1+sqrt(1 + 4*|.p.|*|.p.|))^2; then
    A79: 1-|.q.|*|.q.| = (1+sqrt(1 + 4*|.p.|*|.p.|))^2/
    (1+sqrt(1 + 4*|.p.|*|.p.|))^2
    -4*|.p.|*|.p.|/(1+sqrt(1 + 4*|.p.|*|.p.|))^2 by A78,XCMPLX_1:60
    .= (1+2*sqrt(1 + 4*|.p.|*|.p.|)+(sqrt(1 + 4*|.p.|*|.p.|))^2-4*|.p.|*|.p.|)/
    (1+sqrt(1 + 4*|.p.|*|.p.|))^2
    .= (1+2*sqrt(1 + 4*|.p.|*|.p.|)+(1 + 4*|.p.|*|.p.|)-4*|.p.|*|.p.|)/
    (1+sqrt(1 + 4*|.p.|*|.p.|))^2 by SQUARE_1:def 4
    .= 2*(1+sqrt(1 + 4*|.p.|*|.p.|))/
    ((1+sqrt(1 + 4*|.p.|*|.p.|))*(1+sqrt(1 + 4*|.p.|*|.p.|)))
    .= 2/(1+sqrt(1 + 4*|.p.|*|.p.|)) by A78,XCMPLX_1:92;
    f.(f14.x) = 1/(2/(1+sqrt(1 + 4*|.p.|*|.p.|))) * q by A2,A79
    .= (1+sqrt(1 + 4*|.p.|*|.p.|))/2 * q by XCMPLX_1:57
    .= (1+sqrt(1 + 4*|.p.|*|.p.|))/2*(2/(1+sqrt(1 + 4*|.p.|*|.p.|)))*p
    by A77,EUCLID:34
    .= (2*(1+sqrt(1 + 4*|.p.|*|.p.|)))/(2*(1+sqrt(1 + 4*|.p.|*|.p.|)))*p
    by XCMPLX_1:77
    .= 1*p by A78,XCMPLX_1:60 .= p by EUCLID:33; then
    [f14.x,x] in f by A76,FUNCT_1:def 4; then
    [x,f14.x] in g~ by RELAT_1:def 7; then
    [x,f14.x] in g" by A35,FUNCT_1:def 9;
    hence f14.x = f".x by A74,FUNCT_1:8;
  end; then
  f" is continuous by PRE_TOPC:57,A72,FUNCT_1:9;
  hence thesis by A3,A14,A35,A44,A48,TOPS_2:def 5;
end;

:: like TOPREALB:19
theorem Th7:
  for r being positive (real number),
      f being Function of Tunit_ball(n), Tball(p,r) st n <> 0
  & for a being Point of Tunit_ball(n), b being Point of TOP-REAL n
      st a = b holds f.a = r*b+p
  holds f is being_homeomorphism
proof
  let r be positive (real number),
  f being Function of Tunit_ball(n), Tball(p,r) such that
  A1: n <> 0 and
  A2: for a being Point of Tunit_ball(n), b being Point of TOP-REAL n st
  a = b holds f.a = r*b+p;
  reconsider n1 = n as non empty Element of NAT by A1,ORDINAL1:def 13;
  reconsider x = p as Point of TOP-REAL n1;
  defpred P[Point of TOP-REAL n1,set] means $2 = r*$1+x;
  set U = Tunit_ball(n), B = Tball(x,r);
  A3: for u being Point of TOP-REAL n1
  ex y being Point of TOP-REAL n1 st P[u,y];
  consider F being Function of TOP-REAL n1, TOP-REAL n1 such that
  A4: for x being Point of TOP-REAL n1 holds P[x,F.x] from FUNCT_2:sch 3(A3);
  defpred R[Point of TOP-REAL n1,set] means $2 = 1/r*($1-x);
  A5: for u being Point of TOP-REAL n1
  ex y being Point of TOP-REAL n1 st R[u,y];
  consider G being Function of TOP-REAL n1, TOP-REAL n1 such that
  A6: for a being Point of TOP-REAL n1 holds R[a,G.a] from FUNCT_2:sch 3(A5);
  set f2 = (TOP-REAL n1) --> x;
  set f1 = id TOP-REAL n1;
  dom G = the carrier of TOP-REAL n by FUNCT_2:def 1; then
  A7: dom (G|Ball(x,r)) = Ball(x,r) by RELAT_1:91;
  for p being Point of TOP-REAL n1 holds G.p = 1/r * f1.p + (-1/r) * f2.p
  proof
    let p be Point of TOP-REAL n1;
    thus 1/r * f1.p + (-1/r) * f2.p = 1/r*p + (-1/r)*f2.p by FUNCT_1:35
    .= 1/r*p + (-1/r)*x by FUNCOP_1:13 .= 1/r*p - 1/r*x by EUCLID:44
    .= 1/r*(p-x) by EUCLID:53 .= G.p by A6;
  end; then
  A8: G is continuous by TOPALG_1:17;
  A9: dom f = [#]U by FUNCT_2:def 1;
  A10: dom f = the carrier of U by FUNCT_2:def 1;
  for p being Point of TOP-REAL n1 holds F.p = r * f1.p + 1 * f2.p
  proof
    let p be Point of TOP-REAL n1;
    thus r * f1.p + 1 * f2.p = r*f1.p + f2.p by EUCLID:33
    .= r*p + f2.p by FUNCT_1:35 .= r*p + x by FUNCOP_1:13 .= F.p by A4;
  end;
  then
  A11: F is continuous by TOPALG_1:17;
  A12: the carrier of B = Ball(x,r) by Th4;
  A13: the carrier of U = Ball(0.TOP-REAL n,1) by Th4;
  A14: for a being set st a in dom f holds f.a = (F|Ball(0.TOP-REAL n,1)).a
  proof
    let a be set such that
    A15: a in dom f;
    reconsider y = a as Point of TOP-REAL n1 by A15,PRE_TOPC:55;
    thus f.a = r*y+x by A2,A15 .= F.y by A4
    .= (F|Ball(0.TOP-REAL n,1)).a by A13,A15,FUNCT_1:72;
  end;
  A16: 1/r*r = 1 by XCMPLX_1:88;
  A17: rng f = [#]B
  proof
    now
      let b be set;
      assume A18: b in [#]B;
      then reconsider c = b as Point of TOP-REAL n1 by PRE_TOPC:55;
      reconsider r1=1/r as Real;
      set a = r1 * (c - x);
      A19: |.a-0.TOP-REAL n1.| = |.a.| by RLVECT_1:26
      .= abs(r1)*|. c-x .| by TOPRNS_1:8
      .= r1*|. c-x .| by ABSVALUE:def 1;
      |. c-x .| < r by A12,A18,TOPREAL9:7; then
      1/r*|. c-x .| < 1/r*r by XREAL_1:70; then
      A20: a in Ball(0.TOP-REAL n, 1) by A16,A19;
      then f.a = r*a+x by A2,A13 .= r*(1/r)*(c-x)+x by EUCLID:34
      .= c-x+x by A16,EUCLID:33 .= b by EUCLID:52;
      hence b in rng f by A13,A10,A20,FUNCT_1:def 5;
    end; then
    [#]B c= rng f by TARSKI:def 3;
    hence thesis by XBOOLE_0:def 10;
  end;
  now
    let a, b be set such that
    A21: a in dom f and
    A22: b in dom f and
    A23: f.a = f.b;
    reconsider a1 = a, b1 = b as Point of TOP-REAL n1 by A13,A10,A21,A22;
    A24: f.b1 = r*b1+x by A2,A22;
    f.a1 = r*a1+x by A2,A21;
    then r*a1 = r*b1+x-x by A23,A24,EUCLID:52;
    hence a=b by EUCLID:38,52;
  end; then
  A25: f is one-to-one by FUNCT_1:def 8;
  A26: for a being set st a in dom(f") holds f".a = (G|Ball(x,r)).a
  proof
    reconsider ff = f as Function;
    let a be set such that
    A27: a in dom (f");
    reconsider y = a as Point of TOP-REAL n1 by A27,PRE_TOPC:55;
    reconsider r1=1/r as Real;
    set e = 1/r * (y - x);
    A28: |.e-0.TOP-REAL n1.| = |.e.| by RLVECT_1:26
    .= abs(r1)*|. y-x .| by TOPRNS_1:8 .= r1*|. y-x .| by ABSVALUE:def 1;
    |. y-x .| < r by A27,A12,TOPREAL9:7; then
    1/r*|. y-x .| < 1/r*r by XREAL_1:70; then
    A29: 1/r * (y - x) in Ball(0.TOP-REAL n,1) by A16,A28;
    then f.e = r*e+x by A2,A13 .= r*(1/r)*(y-x)+x by EUCLID:34
    .= y-x+x by A16,EUCLID:33 .= y by EUCLID:52;
    then ff".a = 1/r * (y - x) by A13,A10,A25,A29,FUNCT_1:54;
    hence f".a = 1/r*(y-x) by A17,A25,TOPS_2:def 4
    .= G.y by A6 .= (G|Ball(x,r)).a by A12,A27,FUNCT_1:72;
  end;
  dom F = the carrier of TOP-REAL n by FUNCT_2:def 1; then
  dom (F|Ball(0.TOP-REAL n,1)) = Ball(0.TOP-REAL n,1) by RELAT_1:91; then
  A30: f is continuous by A13,A10,A11,A14,BORSUK_4:69,FUNCT_1:9;
  A31: dom (f") = the carrier of B by FUNCT_2:def 1;
  f" is continuous by A31,A12,A7,A8,A26,BORSUK_4:69,FUNCT_1:9;
  hence thesis by A9,A17,A25,A30,TOPS_2:def 5;
end;

theorem Th8:
  Tunit_ball n, TOP-REAL n are_homeomorphic
proof
  reconsider n1 = n as Element of NAT by ORDINAL1:def 13;
  set U = Tunit_ball(n), C = TOP-REAL n;
  per cases;
  suppose A1: n is non empty;
    defpred P[Point of U,set] means ex w being Point of TOP-REAL n1 st w = $1 &
    $2 = 1/(1-|.w.|*|.w.|)*w;
    A2: for u being Point of U ex y being Point of C st P[u,y]
    proof
      let u be Point of U;
      reconsider v = u as Point of TOP-REAL n1 by PRE_TOPC:55;
      set y = 1/(1-|.v.|*|.v.|)*v;
      reconsider y as Point of C;
      take y;
      thus thesis;
    end;
    consider f being Function of U,C such that
    A3: for x being Point of U holds P[x,f.x] from FUNCT_2:sch 3(A2);
    for a being Point of U, b being Point of TOP-REAL n1 st a = b
    holds f.a = 1/(1-|.b.|*|.b.|)*b
    proof
      let a be Point of U, b be Point of TOP-REAL n1;
      P[a,f.a] by A3;
      hence thesis;
    end; then
    ex f being Function of U,C st f is being_homeomorphism by A1,Th6;
    hence thesis by T_0TOPSP:def 1;
  end;
  suppose A4: n is empty;
    A5: for x being set holds x in Ball(0.TOP-REAL 0,1) iff x = 0.TOP-REAL 0
    proof
      let x be set;
      thus x in Ball(0.TOP-REAL 0,1) implies x = 0.TOP-REAL 0;
      assume x = 0.TOP-REAL 0; then
      reconsider p = x as Point of TOP-REAL 0;
      |.p - 0.(TOP-REAL 0).| < 1 by EUCLID_2:61;
      hence x in Ball(0.TOP-REAL 0,1);
    end;
    [#]TOP-REAL 0 = {0.TOP-REAL 0} by JORDAN2C:113,EUCLID:25
    .= Ball(0.TOP-REAL 0,1) by A5,TARSKI:def 1;
    hence thesis by A4,Th1;
  end;
end;

reserve q for Point of TOP-REAL n;

theorem Th9:
  for r,s being positive (real number) holds
  Tball(p,r), Tball(q,s) are_homeomorphic
proof
  let r,s be positive (real number);
  per cases;
  suppose A1: n is empty;
    reconsider n1=n as Element of NAT by ORDINAL1:def 13;
    reconsider p1=p,q1=q as Point of TOP-REAL n1;
    set X = {x where x is Point of TOP-REAL n: |. x - p .| < r};
    set Y = {x where x is Point of TOP-REAL n: |. x - q .| < s};
    A2: p1 = 0.TOP-REAL 0 by A1;
    A3: q1 = 0.TOP-REAL 0 by A1;
    for x being set holds x in X iff x in Y
    proof
      let x be set;
      hereby
        assume x in X; then
        consider x1 be Point of TOP-REAL n such that
        A4: x=x1 & |. x1 - p .| < r;
        reconsider x1 as Point of TOP-REAL n1;
        x1 = 0.TOP-REAL 0 by A1; then
        |. x1 - p1 .| = 0 by A2,TOPRNS_1:29;
        hence x in Y by A2,A3,A4;
      end;
      assume x in Y; then
      consider x1 be Point of TOP-REAL n such that
      A5: x=x1 & |. x1 - q .| < s;
      reconsider x1 as Point of TOP-REAL n1;
      x1 = 0.TOP-REAL 0 by A1; then
      |. x1 - q1 .| = 0 by A3,TOPRNS_1:29;
      hence x in X by A2,A3,A5;
    end;
    hence thesis by TARSKI:2;
  end;
  suppose n is non empty; then
    reconsider n1=n as non empty Element of NAT by ORDINAL1:def 13;
    A6: for r being positive (real number), x being Point of TOP-REAL n1
    holds Tunit_ball(n1), Tball(x,r) are_homeomorphic
    proof
      let r be positive (real number), x be Point of TOP-REAL n1;
      set U = Tunit_ball(n), C = Tball(x,r);
      defpred P[Point of U,set] means
      ex w being Point of TOP-REAL n1 st w = $1 & $2 = r*w+x;
      A7: r is Real by XREAL_0:def 1;
      A8: the carrier of C = Ball(x,r) by Th4;
      A9: for u being Point of U ex y being Point of C st P[u,y]
      proof
        let u be Point of U;
        reconsider v = u as Point of TOP-REAL n1 by PRE_TOPC:55;
        set y = r*v+x;
        A10: |. y-x .| = |. r*v .| by EUCLID:52
        .= abs(r)*|. v .| by A7,TOPRNS_1:8 .= r*|. v .| by ABSVALUE:def 1;
        r*|. v .| < r*1 by Th5,XREAL_1:70; then
        reconsider y as Point of C by A10,A8,TOPREAL9:7;
        take y;
        thus thesis;
      end;
      consider f being Function of U,C such that
      A11: for x being Point of U holds P[x,f.x] from FUNCT_2:sch 3(A9);
      for a being Point of U, b being Point of TOP-REAL n1 st a = b
      holds f.a = r*b+x
      proof
        let a be Point of U, b be Point of TOP-REAL n1;
        P[a,f.a] by A11;
        hence thesis;
      end; then
      ex f being Function of U,C st f is being_homeomorphism by Th7;
      hence thesis by T_0TOPSP:def 1;
    end;
    for x,y being Point of TOP-REAL n1
    holds Tball(x,r), Tball(y,s) are_homeomorphic
    proof
      let x,y be Point of TOP-REAL n1;
      A12: Tunit_ball(n), Tball(y,s) are_homeomorphic by A6;
      Tball(x,r), Tunit_ball(n) are_homeomorphic by A6;
      hence thesis by A12,BORSUK_3:3;
    end;
    hence thesis;
  end;
end;

theorem Th10:
  for B being non empty ball Subset of TOP-REAL n
  holds B, [#]TOP-REAL n are_homeomorphic
proof
  let B be non empty ball Subset of TOP-REAL n;
  consider p be Point of TOP-REAL n, r be real number such that
  A1: B = Ball(p,r) by Def1;
  reconsider B1 = Tball(p,r) as non empty TopSpace by A1;
  A2: TOP-REAL n , (TOP-REAL n) | ([#]TOP-REAL n) are_homeomorphic by Th1;
  A3: Tunit_ball n, TOP-REAL n are_homeomorphic by Th8;
  r is positive by A1; then
  Tball(p,r), Tball(0.(TOP-REAL n),1) are_homeomorphic by Th9; then
  B1, TOP-REAL n are_homeomorphic by A3,BORSUK_3:3; then
  Tball(p,r) , (TOP-REAL n) | ([#]TOP-REAL n) are_homeomorphic
  by A2,BORSUK_3:3;
  hence B, [#]TOP-REAL n are_homeomorphic by A1,METRIZTS:def 1;
end;

theorem Th11:
  for M, N being non empty TopSpace
  for p being Point of M, U being a_neighborhood of p, B being open Subset of N
  st U,B are_homeomorphic
  ex V being open Subset of M, S being open Subset of N
     st V c= U & p in V & V,S are_homeomorphic
proof
  let M, N be non empty TopSpace;
  let p be Point of M;
  let U be a_neighborhood of p;
  let B be open Subset of N;
  assume U,B are_homeomorphic; then
  A1: M|U, N|B are_homeomorphic by METRIZTS:def 1; then
  consider f be Function of M|U, N|B such that
  A2: f is being_homeomorphism by T_0TOPSP:def 1;
  consider V be Subset of M such that
  A3: V is open & V c= U & p in V by CONNSP_2:8;
  V c= [#](M|U) by A3,PRE_TOPC:def 10; then
  reconsider V1 = V as Subset of M|U;
  reconsider M1=M|U as non empty TopStruct by A3;
  reconsider N1=N|B as non empty TopStruct by A3,A1,YELLOW14:19;
  reconsider f1=f as Function of M1, N1;
  rng f c= [#](N|B); then
  A4: rng f c= B by PRE_TOPC:def 10;
  V1, f .: V1 are_homeomorphic by A2,METRIZTS:3; then
  A5: (M|U) | V1 , (N|B) | (f .: V1) are_homeomorphic by METRIZTS:def 1;
  reconsider V as open Subset of M by A3;
  B = the carrier of N|B by PRE_TOPC:29; then
  reconsider N1 = N|B as open SubSpace of N by TSEP_1:16;
  B c= the carrier of N; then
  [#](N|B) c= the carrier of N by PRE_TOPC:def 10; then
  reconsider S = f .: V1 as Subset of N by XBOOLE_1:1;
  reconsider S1 = f .: V1 as Subset of N1;
  A6: for P being Subset of M1 holds P is open iff f1 .: P is open
  by A2,TOPGRP_1:25;
  A7: V in the topology of M by PRE_TOPC:def 5;
  V1 = V /\ [#]M1 by XBOOLE_1:28; then
  V1 in the topology of M1 by A7,PRE_TOPC:def 9; then
  V1 is open by PRE_TOPC:def 5; then
  S1 is open by A6; then
  reconsider S as open Subset of N by TSEP_1:17;
  take V, S;
  thus V c= U & p in V by A3;
  A8: (M | U) | V1 = M | V by A3,PRE_TOPC:28;
  f .: U c= rng f by RELAT_1:144; then
  A9: f .: U c= B by A4,XBOOLE_1:1;
  f .: V c= f .: U by A3,RELAT_1:156; then
  (N | B) | (f .: V1) = N | S by A9,XBOOLE_1:1,PRE_TOPC:28;
  hence V,S are_homeomorphic by A5,A8,METRIZTS:def 1;
end;

begin :: Manifold

reserve M for non empty TopSpace;

definition
  let n, M;
  attr M is n-locally_euclidean means :Def4:
  for p being Point of M holds
  ex U being a_neighborhood of p, S being open Subset of TOP-REAL n
    st U,S are_homeomorphic;
end;

registration
  let n;
  cluster TOP-REAL n -> n-locally_euclidean;
coherence
proof
  let p be Point of TOP-REAL n;
  p in [#]TOP-REAL n; then
  p in Int [#]TOP-REAL n by TOPS_1:43; then
  reconsider U = [#]TOP-REAL n as a_neighborhood of p by CONNSP_2:def 1;
  reconsider S = U as open Subset of TOP-REAL n;
  take U,S;
  thus U,S are_homeomorphic by METRIZTS:1;
end;
end;

registration
  let n;
  cluster n-locally_euclidean (non empty TopSpace);
  correctness
  proof take TOP-REAL n; thus thesis; end;
end;

Lm1: M is n-locally_euclidean implies
  for p being Point of M holds
  ex U being a_neighborhood of p, B being non empty ball Subset of TOP-REAL n
    st U,B are_homeomorphic
proof
  assume A1: M is n-locally_euclidean;
  let p be Point of M;
  consider U be a_neighborhood of p, S be open Subset of TOP-REAL n
  such that A2: U,S are_homeomorphic by A1,Def4;
  consider U1 be open Subset of M, S be open Subset of TOP-REAL n
  such that
  A3: U1 c= U & p in U1 & U1,S are_homeomorphic by A2,Th11;
  reconsider U1 as non empty Subset of M by A3;
  A4: M|U1, (TOP-REAL n) | S are_homeomorphic by A3,METRIZTS:def 1; then
  consider f be Function of M|U1, (TOP-REAL n) | S such that
  A5: f is being_homeomorphism by T_0TOPSP:def 1;
  A6: p in [#](M|U1) by A3,PRE_TOPC:def 10;
  reconsider S1 = (TOP-REAL n) | S as non empty TopSpace by A4,YELLOW14:19;
  reconsider M1 = M|U1 as non empty SubSpace of M;
  reconsider f as Function of M1, S1;
  A7: [#] ((TOP-REAL n) | S) = S by PRE_TOPC:def 10;
  A8: [#] ((TOP-REAL n) | S) c= [#] (TOP-REAL n) by PRE_TOPC:def 9;
  f.p in the carrier of (TOP-REAL n) | S by A6,FUNCT_2:7; then
  reconsider q = f.p as Point of TOP-REAL n by A8;
  consider B be ball Subset of TOP-REAL n such that
  A9: B c= S & q in B by A6,FUNCT_2:7,A7,Th3;
  reconsider B as non empty ball Subset of TOP-REAL n by A9;
  A10: f" is being_homeomorphism by A5,TOPS_2:70;
  reconsider B1 = B as non empty Subset of S1 by A9,A7;
  A11: rng f = [#]S1 by A5,TOPS_2:def 5;
  A12: f is one-to-one by A5,TOPS_2:def 5;
  A13: dom(f") = the carrier of S1 by A11,A12,TOPS_2:62; then
  A14: (f").q in f" .: B1 by A9,FUNCT_1:def 12; then
  reconsider U2 = f" .: B1 as non empty Subset of M1;
  A15: dom(f"|B1) = B1 by A13,RELAT_1:91;
  A16: dom(f"|B1) = [#](S1|B1) by A15,PRE_TOPC:def 10
  .= the carrier of S1|B1;
  rng(f"|B1) = f" .: B1 by RELAT_1:148
  .= [#](M1|U2) by PRE_TOPC:def 10
  .= the carrier of M1|U2; then
  reconsider g = f"|B1 as Function of S1|B1, M1|U2 by A16,FUNCT_2:3;
  A17: g is being_homeomorphism by A10,METRIZTS:2;
  reconsider p1=p as Point of M1 by A6;
  reconsider f1=f as Function;
  A18: f1 is one-to-one & p in dom f1 by A5,TOPS_2:def 5,A6;
  f1"=f" by A12,TOPS_2:def 4,A11; then
  A19: p1 in U2 by A14,A18,FUNCT_1:56;
  A20: [#]M1 c= [#]M by PRE_TOPC:def 9;
  reconsider V = U2 as Subset of M by A20,XBOOLE_1:1;
  A21: B in the topology of TOP-REAL n by PRE_TOPC:def 5;
  B1 = B /\ [#]S1 by XBOOLE_1:28; then
  B1 in the topology of S1 by A21,PRE_TOPC:def 9; then
  B1 is open by PRE_TOPC:def 5; then
  f" .: B1 is open by A10,TOPGRP_1:25; then
  reconsider V as a_neighborhood of p by A19,CONNSP_2:5,CONNSP_2:11;
  take V, B;
  A22: M1|U2, S1|B1 are_homeomorphic by A17,T_0TOPSP:def 1;
  rng(f") c= [#](M|U1); then
  A23: rng(f") c= U1 by PRE_TOPC:def 10;
  f" .: B1 c= rng(f") by RELAT_1:144; then
  A24: M|V = M1|U2 by A23,XBOOLE_1:1,PRE_TOPC:28;
  S1|B1 = (TOP-REAL n) | B by A9,PRE_TOPC:28;
  hence V,B are_homeomorphic by A24,A22,METRIZTS:def 1;
end;

:: Lemma 2.13a
theorem
  M is n-locally_euclidean iff
  for p being Point of M holds
  ex U being a_neighborhood of p, B being ball Subset of TOP-REAL n
    st U,B are_homeomorphic
proof
  hereby
    assume A1: M is n-locally_euclidean;
    let p be Point of M;
    consider U be a_neighborhood of p, B be non empty ball Subset of TOP-REAL n
    such that A2: U,B are_homeomorphic by A1,Lm1;
    reconsider B as ball Subset of TOP-REAL n;
    take U, B;
    thus U, B are_homeomorphic by A2;
  end;
  assume A3: for p being Point of M holds
  ex U being a_neighborhood of p, B being ball Subset of TOP-REAL n
  st U,B are_homeomorphic;
  now
    let p be Point of M;
    consider U be a_neighborhood of p, B be ball Subset of TOP-REAL n
    such that A4: U,B are_homeomorphic by A3;
    reconsider S = B as open Subset of TOP-REAL n;
    take U, S;
    thus U,S are_homeomorphic by A4;
  end;
  hence M is n-locally_euclidean by Def4;
end;

:: Lemma 2.13b
theorem Th13:
  M is n-locally_euclidean iff
  for p being Point of M holds
  ex U being a_neighborhood of p st U,[#]TOP-REAL n are_homeomorphic
proof
  hereby
    assume A1: M is n-locally_euclidean;
    let p be Point of M;
    consider U be a_neighborhood of p, B be non empty ball Subset of TOP-REAL n
    such that A2: U,B are_homeomorphic by A1,Lm1;
    take U;
    A3: (TOP-REAL n) | ([#]TOP-REAL n) = the TopStruct of TOP-REAL n
    by TSEP_1:100;
    reconsider B1 = (TOP-REAL n) | B as non empty TopSpace;
    M|U,B1 are_homeomorphic by A2,METRIZTS:def 1; then
    reconsider U1 = M|U as non empty TopSpace by YELLOW14:19;
    A4: U1,B1 are_homeomorphic by A2,METRIZTS:def 1;
    B, [#]TOP-REAL n are_homeomorphic by Th10; then
    A5: B1, the TopStruct of TOP-REAL n are_homeomorphic by A3,METRIZTS:def 1;
    U1, the TopStruct of TOP-REAL n are_homeomorphic by A4,A5,BORSUK_3:3;
    hence U,[#]TOP-REAL n are_homeomorphic by A3,METRIZTS:def 1;
  end;
  assume A6: for p being Point of M holds
  ex U being a_neighborhood of p st U,[#]TOP-REAL n are_homeomorphic;
  now
    let p be Point of M;
    consider U be a_neighborhood of p
    such that A7: U,[#]TOP-REAL n are_homeomorphic by A6;
    set S =the  non empty ball Subset of TOP-REAL n;
    A8: S,[#]TOP-REAL n are_homeomorphic by Th10;
    reconsider S as open Subset of TOP-REAL n;
    take U, S;
    A9: (TOP-REAL n) | ([#]TOP-REAL n) = the TopStruct of TOP-REAL n
    by TSEP_1:100;
    A10: M|U,the TopStruct of TOP-REAL n are_homeomorphic
    by A7,A9,METRIZTS:def 1; then
    reconsider U1 = M|U as non empty TopSpace by YELLOW14:19;
    reconsider S1 = (TOP-REAL n) | S as non empty TopSpace;
    A11: the TopStruct of TOP-REAL n, S1 are_homeomorphic
    by A8,A9,METRIZTS:def 1;
    U1, S1 are_homeomorphic by A10,A11,BORSUK_3:3;
    hence U,S are_homeomorphic by METRIZTS:def 1;
  end;
  hence M is n-locally_euclidean by Def4;
end;

registration
  let n;
  cluster n-locally_euclidean -> first-countable (non empty TopSpace);
  correctness
  proof
    let M be non empty TopSpace;
    assume A1: M is n-locally_euclidean;
    for p being Point of M ex B being Basis of p st B is countable
    proof
      let p be Point of M;
      consider U be a_neighborhood of p such that
      A2: U,[#]TOP-REAL n are_homeomorphic by A1,Th13;
      M|U, (TOP-REAL n) | ([#]TOP-REAL n) are_homeomorphic
      by A2,METRIZTS:def 1; then
      M|U, the TopStruct of TOP-REAL n are_homeomorphic by TSEP_1:100; then
      consider f be Function of M|U, the TopStruct of TOP-REAL n such that
      A3: f is being_homeomorphism by T_0TOPSP:def 1;
      A4: dom f = [#](M|U) & rng f = [#](the TopStruct of TOP-REAL n) &
      f is one-to-one & f is continuous &
      f" is continuous by A3,TOPS_2:def 5; then
      A5: dom f = U by PRE_TOPC:def 10;
      A6: Int U c= U by TOPS_1:44;
      A7: p in Int U by CONNSP_2:def 1;
      A8: p in dom f by A7,A6,A5;
      f.p in rng f by A7,A6,A5,FUNCT_1:12; then
      reconsider q=f.p as Point of TOP-REAL n;
      reconsider n1=n as Element of NAT by ORDINAL1:def 13;
      TOP-REAL n1 is first-countable; then
      consider B1 be Basis of q such that
      A9: B1 is countable by FRECHET:def 2;
      reconsider A = bool the carrier of TOP-REAL n as non empty set;
      deffunc F(set) = f" .: $1 /\ Int U;
      set B = {F(X) where X is Element of A: X in B1};
      A10: card B1 c= omega by A9,CARD_3:def 15;
      card B c= card B1 from TREES_2:sch 2; then
      A11: card B c= omega by A10,XBOOLE_1:1;
      for x being set st x in B holds x in bool the carrier of M
      proof
        let x be set;
        assume x in B; then
        consider X1 be Element of A such that
        A12: x = F(X1) & X1 in B1;
        thus x in bool the carrier of M by A12;
      end; then
      reconsider B as Subset-Family of M by TARSKI:def 3;
      A13: for P being Subset of M st P in B holds P is open
      proof
        let P be Subset of M;
        assume P in B; then
        consider X1 be Element of A such that
        A14: P = F(X1) & X1 in B1;
        reconsider X1 as Subset of the TopStruct of TOP-REAL n;
        reconsider X2 = X1 as Subset of TOP-REAL n;
        X2 is open by A14,YELLOW_8:21; then
        X2 in the topology of TOP-REAL n by PRE_TOPC:def 5; then
        A15: X1 is open by PRE_TOPC:def 5;
        reconsider U1 = M|U as non empty TopStruct by A7,A6;
        reconsider g = f" as Function of the TopStruct of TOP-REAL n, U1;
        A16: g is being_homeomorphism by A3,TOPS_2:70;
        A17: g .: X1 is open by A15,A16,TOPGRP_1:25;
        g .: X1 in the topology of M|U by A17,PRE_TOPC:def 5; then
        consider Q be Subset of M such that
        A18: Q in the topology of M &
        g .: X1 = Q /\ [#](M|U) by PRE_TOPC:def 9;
        [#](M|U) = U by PRE_TOPC:def 10; then
        A19: P = Q /\ (U /\ Int U) by A18,A14,XBOOLE_1:16
        .= Q /\ Int U by TOPS_1:44,XBOOLE_1:28;
        Q is open by A18,PRE_TOPC:def 5;
        hence P is open by A19;
      end;
      for Y being set st Y in B holds p in Y
      proof
        let Y be set;
        assume Y in B; then
        consider X1 be Element of A such that
        A20: Y = F(X1) & X1 in B1;
        reconsider g = f as Function;
        [p,g.p] in g by A7,A6,A5,FUNCT_1:def 4; then
        [q,p] in g~ by RELAT_1:def 7; then
        [q,p] in g" by A4,FUNCT_1:def 9; then
        A21: [q,p] in f" by A4,TOPS_2:def 4;
        q in X1 by A20,YELLOW_8:21; then
        p in f" .: X1 by A21,RELAT_1:def 13;
        hence p in Y by A20,A7,XBOOLE_0:def 4;
      end; then
      A22: p in Intersect B by SETFAM_1:58;
      for S being Subset of M st S is open & p in S holds
      ex V being Subset of M st V in B & V c= S
      proof
        let S be Subset of M;
        assume A23: S is open & p in S;
        set S1 = S /\ [#](M|U);
        S in the topology of M by A23,PRE_TOPC:def 5; then
        A24: S1 in the topology of M|U by PRE_TOPC:def 9;
        reconsider U1 = M|U as non empty TopStruct by A7,A6;
        reconsider S1 as Subset of U1;
        S1 is open by A24,PRE_TOPC:def 5; then
        A25: f .: S1 is open by A3,TOPGRP_1:25;
        reconsider S2 = f .: S1 as Subset of TOP-REAL n;
        f .: S1 in the topology of the TopStruct of TOP-REAL n
        by A25,PRE_TOPC:def 5; then
        A26: S2 is open by PRE_TOPC:def 5;
        reconsider g1 = f as Function;
        A27: [p,q] in f by A7,A6,A5,FUNCT_1:def 4;
        p in S1 by A8,A23,XBOOLE_0:def 4; then
        A28: q in S2 by A27,RELAT_1:def 13;
        consider W be Subset of TOP-REAL n such that
        A29: W in B1 & W c= S2 by A28,A26,YELLOW_8:22;
        reconsider W as Element of A;
        set V = f" .: W /\ Int U;
        reconsider V as Subset of M;
        take V;
        thus V in B by A29;
        A30: g1" = f" by A4,TOPS_2:def 4;
        A31: f" .: (f .: S1) = S1 by A30,A4,FUNCT_1:177;
        A32: f" .: W /\ Int U c= f" .: W by XBOOLE_1:17;
        A33: S1 c= S by XBOOLE_1:17;
        f" .: W c= f" .: (f .: S1) by A29,RELAT_1:156; then
        f" .: W c= S by A31,A33,XBOOLE_1:1;
        hence V c= S by A32,XBOOLE_1:1;
      end; then
      reconsider B as Basis of p by A13,A22,YELLOW_8:def 2,TOPS_2:def 1;
      take B;
      thus B is countable by A11,CARD_3:def 15;
    end;
    hence M is first-countable by FRECHET:def 2;
  end;
end;

set T = (TOP-REAL 0) | [#]TOP-REAL 0;
Lm2: T = the TopStruct of TOP-REAL 0 by TSEP_1:100;

registration
  cluster 0-locally_euclidean -> discrete (non empty TopSpace);
  coherence
  proof
    let M be non empty TopSpace;
    assume A1: M is 0-locally_euclidean;
    for X being Subset of M, p being Point of M st X = {p} holds X is open
    proof
      let X be Subset of M;
      let p be Point of M;
      assume A2: X = {p};
      consider U be a_neighborhood of p such that
      A3: U,[#]TOP-REAL 0 are_homeomorphic by A1,Th13;
      A4: Int U c= U by TOPS_1:44;
      p in Int U by CONNSP_2:def 1; then
      A5: p in U by A4;
      M|U, T are_homeomorphic by A3,METRIZTS:def 1; then
      consider f be Function of M|U, T such that
      A6: f is being_homeomorphism by T_0TOPSP:def 1;
      consider V be Subset of M such that
      A7: V is open & V c= U & p in V by CONNSP_2:8;
      for x being set holds x in V iff x = p
      proof
        let x be set;
        hereby
          assume x in V; then
          A8: x in U by A7;
          A9: f is one-to-one by A6,TOPS_2:def 5;
          x in [#](M|U) by A8,PRE_TOPC:def 10; then
          A10: x in dom f by A6,TOPS_2:def 5; then
          A11: f.x in rng f by FUNCT_1:12;
          p in [#](M|U) by A5,PRE_TOPC:def 10; then
          A12: p in dom f by A6,TOPS_2:def 5; then
          A13: f.p in rng f by FUNCT_1:12;
          f.x = 0.TOP-REAL 0 by Lm2,A11 .= f.p by Lm2,A13;
          hence x = p by A9,A10,A12,FUNCT_1:def 8;
        end;
        assume x = p;hence x in V by A7;
      end;
      hence X is open by A2,A7,TARSKI:def 1;
    end;
    hence M is discrete by TDLAT_3:19;
  end;
  cluster discrete -> 0-locally_euclidean (non empty TopSpace);
  coherence
  proof
  A14: [#]T = {0.TOP-REAL 0} by EUCLID:25,JORDAN2C:113,Lm2;
  let M be non empty TopSpace;
  assume A15: M is discrete;
  for p being Point of M holds
  ex U being a_neighborhood of p st U,[#]TOP-REAL 0 are_homeomorphic
  proof
    let p be Point of M;
    reconsider U = {p} as Subset of M by ZFMISC_1:37;
    A16: U is open & p in U by A15,TDLAT_3:17,TARSKI:def 1; then
    reconsider U as a_neighborhood of p by CONNSP_2:5;
    take U;
    set f = {[p, 0.TOP-REAL 0]};
    A17: p in [#](M|U) by A16,PRE_TOPC:def 10;
    A18: [p, 0.TOP-REAL 0] in [: the carrier of M|U , the carrier of T :]
    by A17,ZFMISC_1:106,Lm2;
    A19: dom f = U by RELAT_1:23; then
    A20: dom f = [#](M|U) by PRE_TOPC:def 10; then
    reconsider f as Function of M|U, T by A18,FUNCT_2:def 1,ZFMISC_1:37;
    A21: rng f = [#]T by A14,RELAT_1:23;
    for P being Subset of M|U holds P is closed iff f .: P is closed
    proof
      let P be Subset of M|U;
      per cases;
      suppose A22: P is empty; then f.:P is empty by RELAT_1:149;
        hence thesis by A22;
      end;
      suppose A23: P is non empty; then
        P = [#](M|U) by A20,ZFMISC_1:39,A19;
        hence P is closed implies f.:P is closed by A21,A20,RELAT_1:146;
        thus f.:P is closed implies P is closed by A23,A20,ZFMISC_1:39,A19;
      end;
    end; then
    f is being_homeomorphism by A20,A21,TOPS_2:72; then
    M|U, T are_homeomorphic by T_0TOPSP:def 1;
    hence U,[#]TOP-REAL 0 are_homeomorphic by METRIZTS:def 1;
  end;
  hence M is 0-locally_euclidean by Th13;
  end;
end;

registration
  let n;
  cluster TOP-REAL n -> second-countable;
  correctness
  proof
    set T = the TopStruct of TOP-REAL n;
    A1: for x being set holds
    x in {card B where B is Basis of T : not contradiction} iff
    x in {card B where B is Basis of TOP-REAL n : not contradiction}
    proof
      let x be set;
      hereby
        assume x in {card B where B is Basis of T : not contradiction}; then
        consider B1 be Basis of T such that
        A2: x = card B1;
        reconsider B2=B1 as Basis of TOP-REAL n by YELLOW12:32;
        x = card B2 by A2;
        hence x in {card B where B is Basis of TOP-REAL n : not contradiction};
      end;
      assume x in {card B where B is Basis of TOP-REAL n : not contradiction};
      then consider B1 be Basis of TOP-REAL n such that
      A3: x = card B1;
      reconsider B2=B1 as Basis of T by YELLOW12:32;
      x = card B2 by A3;
      hence x in {card B where B is Basis of T : not contradiction};
    end;
    weight T = weight TOP-REAL n by A1,TARSKI:2; then
    weight TOP-REAL n c= omega by WAYBEL23:def 6;
    hence thesis by WAYBEL23:def 6;
  end;
end;

registration
  let n;
  cluster second-countable Hausdorff n-locally_euclidean (non empty TopSpace);
  existence
  proof take TOP-REAL n; thus thesis; end;
end;

definition
  let n, M;
  attr M is n-manifold means :Def5:
  M is second-countable Hausdorff n-locally_euclidean;
end;

definition
  let M;
  attr M is manifold-like means :Def6:
  ex n st M is n-manifold;
end;

registration
  let n;
  cluster n-manifold (non empty TopSpace);
  existence
  proof
    take TOP-REAL n;
    thus thesis by Def5;
  end;
end;

registration
  let n;
  cluster n-manifold ->
          second-countable Hausdorff n-locally_euclidean (non empty TopSpace);
  correctness by Def5;
  cluster second-countable Hausdorff n-locally_euclidean ->
          n-manifold (non empty TopSpace);
  correctness by Def5;
  cluster n-manifold -> manifold-like (non empty TopSpace);
  correctness by Def6;
end;

registration
  cluster second-countable discrete -> 0-manifold (non empty TopSpace);
  coherence;
end;

:: Lemma 2.16
registration
  let n;
  let M be n-manifold (non empty TopSpace);
  cluster open -> n-manifold (non empty SubSpace of M);
  correctness
  proof
    let X be non empty SubSpace of M;
    assume A1: X is open;
    [#]X c= [#]M by PRE_TOPC:def 9; then
    reconsider X1 = [#]X as non empty open Subset of M
    by A1,TSEP_1:def 1;
    A2: the carrier of X = [#](M|X1) by PRE_TOPC:def 10
    .= the carrier of M|X1; then
    A3: the TopStruct of X = the TopStruct of M|X1 by TSEP_1:5;
    A4: for x being set holds
    x in {card B where B is Basis of X : not contradiction} iff
    x in {card B where B is Basis of M|X1 : not contradiction}
    proof
      let x be set;
      hereby
        assume x in {card B where B is Basis of X : not contradiction}; then
        consider B1 be Basis of X such that
        A5: x = card B1;
        reconsider B2=B1 as Basis of M|X1 by A3,YELLOW12:32;
        x = card B2 by A5;
        hence x in {card B where B is Basis of M|X1 : not contradiction};
      end;
      assume x in {card B where B is Basis of M|X1 : not contradiction};
      then consider B1 be Basis of M|X1 such that
      A6: x = card B1;
      reconsider B2=B1 as Basis of X by A3,YELLOW12:32;
      x = card B2 by A6;
      hence x in {card B where B is Basis of X : not contradiction};
    end;
    weight X = weight M|X1 by A4,TARSKI:2; then
    weight X c= omega by WAYBEL23:def 6; then
    A7: X is second-countable by WAYBEL23:def 6;
    for p being Point of X holds
    ex U being a_neighborhood of p, S being open Subset of TOP-REAL n
    st U,S are_homeomorphic
    proof
      let p be Point of X;
      p in the carrier of X; then
      reconsider p1 = p as Point of M by A2;
      consider U1 be a_neighborhood of p1, S1 be open Subset of TOP-REAL n
      such that
      A8: U1, S1 are_homeomorphic by Def4;
      consider U2 be open Subset of M, S2 be open Subset of TOP-REAL n
      such that
      A9: U2 c= U1 & p1 in U2 & U2, S2 are_homeomorphic by A8,Th11;
      reconsider X2 = X as open (non empty SubSpace of M) by A1;
      reconsider U = U2 /\ X1 as Subset of X2 by XBOOLE_1:17;
      A10: M|U2, (TOP-REAL n) | S2 are_homeomorphic by A9,METRIZTS:def 1; then
      consider f be Function of M|U2, (TOP-REAL n) | S2 such that
      A11: f is being_homeomorphism by T_0TOPSP:def 1;
      A12: p in U2 /\ X1 by A9,XBOOLE_0:def 4;
      U is open by TSEP_1:17; then
      reconsider U as a_neighborhood of p by A12,CONNSP_2:5;
      U c= U2 by XBOOLE_1:17; then
      U c= [#](M|U2) by PRE_TOPC:def 10; then
      reconsider U3 = U as Subset of M|U2;
      U3, f.:U3 are_homeomorphic by A11,METRIZTS:3; then
      A13: (M|U2) | U3, ((TOP-REAL n) |S2 ) | (f.:U3) are_homeomorphic
      by METRIZTS:def 1;
      reconsider M2 = M|U2 as non empty SubSpace of M by A9;
      reconsider T2 = (TOP-REAL n) | S2 as non empty SubSpace of TOP-REAL n
      by A10,A9,YELLOW14:19;
      reconsider f2 = f as Function of M2, T2;
      A14: for P being Subset of M2 holds P is open iff f2.:P is open
      by A11,TOPGRP_1:25;
      f.:U3 c= [#]((TOP-REAL n) | S2); then
      A15: f.:U3 c= S2 by PRE_TOPC:def 10;
      A16: X1 in the topology of M by PRE_TOPC:def 5;
      U2 = [#]M2 by PRE_TOPC:def 10; then
      U3 in the topology of M2 by A16,PRE_TOPC:def 9; then
      U3 is open by PRE_TOPC:def 5; then
      reconsider S = f.:U3 as open Subset of T2 by A14;
      S in the topology of T2 by PRE_TOPC:def 5; then
      consider Q be Subset of TOP-REAL n such that
      A17: Q in the topology of TOP-REAL n & S=Q/\([#]T2) by PRE_TOPC:def 9;
      A18: [#]T2 = S2 by PRE_TOPC:def 10;
      S2 in the topology of TOP-REAL n by PRE_TOPC:def 5; then
      S in the topology of TOP-REAL n by A18,A17,PRE_TOPC:def 1; then
      reconsider S as open Subset of TOP-REAL n by PRE_TOPC:def 5;
      take U, S;
      U c= X1; then U c= [#](M|X1) by PRE_TOPC:def 10; then
      reconsider U4 = U as Subset of M|X1;
      reconsider U5 = U as Subset of M;
      A19: M|X1|U4 = M|U5 by GOBOARD9:4;
      M|U2|U3 = M|U5 by GOBOARD9:4; then
      A20: the TopStruct of X|U = the TopStruct of M|U2|U3
      by A19,A3,PRE_TOPC:66;
      ((TOP-REAL n) | S2) | (f.:U3) = (TOP-REAL n) | S by A15,PRE_TOPC:28;
      hence U, S are_homeomorphic by A13,A20,METRIZTS:def 1;
    end; then
    X is n-locally_euclidean by Def4;
    hence X is n-manifold by A7;
  end;
end;

registration
  cluster manifold-like (non empty TopSpace);
  existence
  proof
    take TOP-REAL 0;
    thus thesis;
  end;
end;

definition
  mode manifold is manifold-like (non empty TopSpace);
end;