mfold_1.miz

    begin

    registration

      let x,y be set;

      cluster { [x, y]} -> one-to-one;

      correctness

      proof

        set f = { [x, y]};

        let x1,x2 be object;

        assume x1 in ( dom f) & x2 in ( dom f) & (f . x1) = (f . x2);

        then

         A1: x1 in {x} & x2 in {x} by RELAT_1: 9;



        hence x1 = x by TARSKI:def 1

        .= x2 by A1, TARSKI:def 1;

      end;

    end

    reserve n for Nat;

    ::$Canceled

    theorem :: MFOLD_1:2



     Th2: for X be non empty SubSpace of ( TOP-REAL n), f be Function of X, R^1 st f is continuous holds ex g be Function of X, ( TOP-REAL n) st (for a be Point of X, b be Point of ( TOP-REAL n), r be Real 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 be Point of ( TOP-REAL n), r be Real st $1 = b & (f . $1) = r holds $2 = (r * b);



       A2: for x be Element of X holds ex y be Point of ( TOP-REAL n) st P[x, y]

      proof

        let x be Element of X;

        reconsider r = (f . x) as Real;

        ( [#] X) c= ( [#] ( TOP-REAL n)) by PRE_TOPC:def 4;

        then

        reconsider p = x as Point of ( TOP-REAL n);

        set y = (r * p);

        take y;

        thus P[x, y];

      end;

      ex g be Function of the carrier of X, the carrier of ( TOP-REAL n) st for x be 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

       A3: for x be Element of X holds for b be Point of ( TOP-REAL n), r be Real st x = b & (f . x) = r holds (g . x) = (r * b);

      take g;

      for p be Point of X, V be Subset of ( TOP-REAL n) st (g . p) in V & V is open holds ex W be 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);

        reconsider n1 = n as Element of NAT by ORDINAL1:def 12;

        reconsider gp = (g . p) as Point of ( Euclid n) by TOPREAL3: 8;

        ( [#] X) c= ( [#] ( TOP-REAL n)) by PRE_TOPC:def 4;

        then

        reconsider pp = p as Point of ( TOP-REAL n1);

        reconsider fp = (f . p) as Real;

        assume (g . p) in V & V is open;

        then (g . p) in ( Int V) by TOPS_1: 23;

        then

        consider r0 be Real such that

         A4: r0 > 0 and

         A5: ( Ball (gp,r0)) c= V by GOBOARD6: 5;

        per cases ;

          suppose

           A6: 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 2;

          then W2 in the topology of X by PRE_TOPC:def 4;

          then

           A7: W2 is open by PRE_TOPC:def 2;

          p in ( Ball (pp,(r0 / 2))) by A4, JORDAN: 16;

          then

           A8: p in W2 by XBOOLE_0:def 4;

          set WW2 = { |.p2.| where p2 be Point of ( TOP-REAL n) : p2 in W2 };



           A9: |.pp.| in WW2 by A8;

          for x be object st x in WW2 holds x is real

          proof

            let x be object;

            assume x in WW2;

            then

            consider p2 be Point of ( TOP-REAL n1) such that

             A10: x = |.p2.| & p2 in W2;

            thus x is real by A10;

          end;

          then

          reconsider WW2 as non empty real-membered set by A9, MEMBERED:def 3;

          for x be ExtReal st x in WW2 holds x <= ( |.pp.| + (r0 / 2))

          proof

            let x be ExtReal;

            assume x in WW2;

            then

            consider p2 be Point of ( TOP-REAL n1) such that

             A11: x = |.p2.| & p2 in W2;

            p2 in ( Ball (pp,(r0 / 2))) by A11, XBOOLE_0:def 4;

            then

             A12: |.(p2 - pp).| < (r0 / 2) by TOPREAL9: 7;

            ( |.p2.| - |.( - pp).|) <= |.(p2 + ( - pp)).| by TOPRNS_1: 31;

            then ( |.p2.| - |.pp.|) <= |.(p2 + ( - pp)).| by TOPRNS_1: 26;

            then ( |.p2.| - |.pp.|) <= (r0 / 2) by A12, XXREAL_0: 2;

            then (( |.p2.| - |.pp.|) + |.pp.|) <= ((r0 / 2) + |.pp.|) by XREAL_1: 6;

            hence x <= ( |.pp.| + (r0 / 2)) by A11;

          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;



           A13: m >= 0

          proof

            assume

             A14: m < 0 ;



             A15: m is UpperBound of WW2 by XXREAL_2:def 3;

             |.pp.| in WW2 by A8;

            hence contradiction by A14, A15, XXREAL_2:def 1;

          end;

          per cases by A13;

            suppose

             A16: m = 0 ;

            set G1 = REAL ;

             REAL in the topology of R^1 by PRE_TOPC:def 1, TOPMETR: 17;

            then

            reconsider G1 as open Subset of R^1 by PRE_TOPC:def 2;

            fp in G1 by XREAL_0:def 1;

            then

            consider W1 be Subset of X such that

             A17: p in W1 and

             A18: W1 is open and (f .: W1) c= G1 by A1, JGRAPH_2: 10;

            reconsider W3 = (W1 /\ W2) as Subset of X;

            take W3;

            thus p in W3 by A17, A8, XBOOLE_0:def 4;

            thus W3 is open by A18, A7;

            (g .: W3) c= ( Ball (gp,r0))

            proof

              let x be object;

              assume x in (g .: W3);

              then

              consider q be object such that

               A19: q in ( dom g) and

               A20: q in W3 and

               A21: (g . q) = x by FUNCT_1:def 6;

              reconsider q as Point of X by A19;

              ( [#] X) c= ( [#] ( TOP-REAL n)) by PRE_TOPC:def 4;

              then

              reconsider qq = q as Point of ( TOP-REAL n1);

              reconsider fq = (f . q) as Real;



               A22: x = (fq * qq) by A3, A21;

              then

              reconsider gq = x as Point of ( Euclid n) by TOPREAL3: 8;

              reconsider gpp = gp as Point of ( TOP-REAL n1);

              reconsider gqq = gq as Point of ( TOP-REAL n1) by A22;



               A23: gpp = (fp * pp) by A3;

              reconsider r2 = (fq - fp) as Real;



               A24: ( |.(fq - fp).| * |.qq.|) = ( |.r2.| * |.qq.|)

              .= |.((fq - fp) * qq).| by TOPRNS_1: 7;

              qq in W2 by A20, XBOOLE_0:def 4;

              then |.qq.| in WW2;

              then

               A25: |.qq.| <= m by XXREAL_2: 4;



               A26: gpp = ( 0. ( TOP-REAL n1)) by A23, A6, RLVECT_1: 10;

               |.(gqq + ( - gpp)).| <= ( |.gqq.| + |.( - gpp).|) by EUCLID_2: 52;

              then |.(gqq + ( - gpp)).| <= ( |.gqq.| + |.( 0. ( TOP-REAL n1)).|) by A26, JGRAPH_5: 10;

              then |.(gqq + ( - gpp)).| <= ( |.gqq.| + 0 ) by EUCLID_2: 39;

              then |.(gqq - gpp).| < r0 by A3, A21, A6, A25, A24, A4, A16;

              then gqq in ( Ball (gpp,r0));

              hence x in ( Ball (gp,r0)) by TOPREAL9: 13;

            end;

            hence thesis by A5;

          end;

            suppose

             A27: m > 0 ;

            set G1 = ].(fp - (r0 / m)), (fp + (r0 / m)).[;

            reconsider G1 as open Subset of R^1 by JORDAN6: 35, TOPMETR: 17, XXREAL_1: 225;



             A28: ( 0 + fp) < ((r0 / m) + fp) by A27, A4, XREAL_1: 6;

            (( - (r0 / m)) + fp) < ( 0 + fp) by A27, A4, XREAL_1: 6;

            then

            consider W1 be Subset of X such that

             A29: p in W1 and

             A30: W1 is open and

             A31: (f .: W1) c= G1 by A1, JGRAPH_2: 10, A28, XXREAL_1: 4;

            reconsider W3 = (W1 /\ W2) as Subset of X;

            take W3;

            thus p in W3 by A29, A8, XBOOLE_0:def 4;

            thus W3 is open by A30, A7;

            (g .: W3) c= ( Ball (gp,r0))

            proof

              let x be object;

              assume x in (g .: W3);

              then

              consider q be object such that

               A32: q in ( dom g) and

               A33: q in W3 and

               A34: (g . q) = x by FUNCT_1:def 6;

              reconsider q as Point of X by A32;



               A35: q in the carrier of X;

              ( [#] X) c= ( [#] ( TOP-REAL n)) by PRE_TOPC:def 4;

              then

              reconsider qq = q as Point of ( TOP-REAL n1);

              reconsider fq = (f . q) as Real;



               A36: x = (fq * qq) by A3, A34;

              then

              reconsider gq = x as Point of ( Euclid n) by TOPREAL3: 8;

              reconsider gpp = gp as Point of ( TOP-REAL n1);

              reconsider gqq = gq as Point of ( TOP-REAL n1) by A36;



               A37: gpp = (fp * pp) by A3;

              reconsider r2 = fq as Real;



               A38: ( |.fq.| * |.qq.|) = ( |.r2.| * |.qq.|)

              .= |.(fq * qq).| by TOPRNS_1: 7;



               A39: q in ( dom f) by A35, FUNCT_2:def 1;

              q in W1 by A33, XBOOLE_0:def 4;

              then (f . q) in (f .: W1) by A39, FUNCT_1:def 6;

              then |.(fq - fp).| < (r0 / m) by A31, RCOMP_1: 1;

              then ( |.fq.| * m) < ((r0 / m) * m) by A6, A27, XREAL_1: 68;

              then ( |.fq.| * m) < (r0 / (m / m)) by XCMPLX_1: 82;

              then

               A40: ( |.fq.| * m) < (r0 / 1) by A27, XCMPLX_1: 60;

              qq in W2 by A33, XBOOLE_0:def 4;

              then |.qq.| in WW2;

              then |.qq.| <= m by XXREAL_2: 4;

              then

               A41: ( |.qq.| * |.fq.|) <= (m * |.fq.|) by XREAL_1: 64;



               A42: gpp = ( 0. ( TOP-REAL n1)) by A37, A6, RLVECT_1: 10;



               A43: |.gqq.| < r0 by A36, A41, A38, A40, XXREAL_0: 2;

               |.(gqq + ( - gpp)).| <= ( |.gqq.| + |.( - gpp).|) by EUCLID_2: 52;

              then |.(gqq + ( - gpp)).| <= ( |.gqq.| + |.( 0. ( TOP-REAL n1)).|) by A42, JGRAPH_5: 10;

              then |.(gqq + ( - gpp)).| <= ( |.gqq.| + 0 ) by EUCLID_2: 39;

              then |.(gqq - gpp).| < r0 by A43, XXREAL_0: 2;

              then gqq in ( Ball (gpp,r0));

              hence x in ( Ball (gp,r0)) by TOPREAL9: 13;

            end;

            hence thesis by A5;

          end;

        end;

          suppose

           A44: fp <> 0 ;

          reconsider W2 = (( Ball (pp,((r0 / 2) / |.fp.|))) /\ ( [#] X)) as Subset of X;

          ( Ball (pp,((r0 / 2) / |.fp.|))) in the topology of ( TOP-REAL n1) by PRE_TOPC:def 2;

          then W2 in the topology of X by PRE_TOPC:def 4;

          then

           A45: W2 is open by PRE_TOPC:def 2;

          p in ( Ball (pp,((r0 / 2) / |.fp.|))) by A44, A4, JORDAN: 16;

          then

           A46: p in W2 by XBOOLE_0:def 4;

          set WW2 = { |.p2.| where p2 be Point of ( TOP-REAL n) : p2 in W2 };



           A47: |.pp.| in WW2 by A46;

          for x be object st x in WW2 holds x is real

          proof

            let x be object;

            assume x in WW2;

            then

            consider p2 be Point of ( TOP-REAL n1) such that

             A48: x = |.p2.| & p2 in W2;

            thus x is real by A48;

          end;

          then

          reconsider WW2 as non empty real-membered set by A47, MEMBERED:def 3;

          for x be ExtReal st x in WW2 holds x <= ( |.pp.| + ((r0 / 2) / |.fp.|))

          proof

            let x be ExtReal;

            assume x in WW2;

            then

            consider p2 be Point of ( TOP-REAL n1) such that

             A49: x = |.p2.| & p2 in W2;

            p2 in ( Ball (pp,((r0 / 2) / |.fp.|))) by A49, XBOOLE_0:def 4;

            then

             A50: |.(p2 - pp).| < ((r0 / 2) / |.fp.|) by TOPREAL9: 7;

            ( |.p2.| - |.( - pp).|) <= |.(p2 + ( - pp)).| by TOPRNS_1: 31;

            then ( |.p2.| - |.pp.|) <= |.(p2 + ( - pp)).| by TOPRNS_1: 26;

            then ( |.p2.| - |.pp.|) <= ((r0 / 2) / |.fp.|) by A50, XXREAL_0: 2;

            then (( |.p2.| - |.pp.|) + |.pp.|) <= (((r0 / 2) / |.fp.|) + |.pp.|) by XREAL_1: 6;

            hence x <= ( |.pp.| + ((r0 / 2) / |.fp.|)) by A49;

          end;

          then ( |.pp.| + ((r0 / 2) / |.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;



           A51: m >= 0

          proof

            assume

             A52: m < 0 ;



             A53: m is UpperBound of WW2 by XXREAL_2:def 3;

             |.pp.| in WW2 by A46;

            hence contradiction by A52, A53, XXREAL_2:def 1;

          end;

          per cases by A51;

            suppose

             A54: m = 0 ;

            set G1 = REAL ;

             REAL in the topology of R^1 by PRE_TOPC:def 1, TOPMETR: 17;

            then

            reconsider G1 as open Subset of R^1 by PRE_TOPC:def 2;

            fp in G1 by XREAL_0:def 1;

            then

            consider W1 be Subset of X such that

             A55: p in W1 and

             A56: W1 is open and (f .: W1) c= G1 by A1, JGRAPH_2: 10;

            reconsider W3 = (W1 /\ W2) as Subset of X;

            take W3;

            thus p in W3 by A55, A46, XBOOLE_0:def 4;

            thus W3 is open by A56, A45;

            (g .: W3) c= ( Ball (gp,r0))

            proof

              let x be object;

              assume x in (g .: W3);

              then

              consider q be object such that

               A57: q in ( dom g) and

               A58: q in W3 and

               A59: (g . q) = x by FUNCT_1:def 6;

              reconsider q as Point of X by A57;

              ( [#] X) c= ( [#] ( TOP-REAL n)) by PRE_TOPC:def 4;

              then

              reconsider qq = q as Point of ( TOP-REAL n1);

              reconsider fq = (f . q) as Real;



               A60: x = (fq * qq) by A3, A59;

              then

              reconsider gq = x as Point of ( Euclid n) by TOPREAL3: 8;

              reconsider gpp = gp as Point of ( TOP-REAL n1);

              reconsider gqq = gq as Point of ( TOP-REAL n1) by A60;



               A61: gpp = (fp * pp) by A3;

              reconsider r2 = (fq - fp) as Real;

              reconsider r3 = fp as Real;



               A62: ( |.(fq - fp).| * |.qq.|) = ( |.r2.| * |.qq.|)

              .= |.((fq - fp) * qq).| by TOPRNS_1: 7;

              qq in W2 by A58, XBOOLE_0:def 4;

              then |.qq.| in WW2;

              then

               A63: |.qq.| <= m by XXREAL_2: 4;



               A64: ( |.fp.| * |.(qq - pp).|) = ( |.r3.| * |.(qq - pp).|)

              .= |.(fp * (qq - pp)).| by TOPRNS_1: 7;

              qq in W2 by A58, XBOOLE_0:def 4;

              then qq in ( Ball (pp,((r0 / 2) / |.fp.|))) by XBOOLE_0:def 4;

              then ( |.fp.| * |.(qq - pp).|) < ( |.fp.| * ((r0 / 2) / |.fp.|)) by A44, XREAL_1: 68, TOPREAL9: 7;

              then ( |.fp.| * |.(qq - pp).|) < ((r0 / 2) / ( |.fp.| / |.fp.|)) by XCMPLX_1: 81;

              then

               A65: ( |.fp.| * |.(qq - pp).|) < ((r0 / 2) / 1) by A44, XCMPLX_1: 60;



               A66: ( |.((fq - fp) * qq).| + |.(fp * (qq - pp)).|) < ((r0 / 2) + (r0 / 2)) by A63, A65, A64, A62, A54, XREAL_1: 8;

               |.(((fq - fp) * qq) + (fp * (qq - pp))).| <= ( |.((fq - fp) * qq).| + |.(fp * (qq - pp)).|) by EUCLID_2: 52;

              then

               A67: |.(((fq - fp) * qq) + (fp * (qq - pp))).| < r0 by A66, XXREAL_0: 2;

              (((fq - fp) * qq) + (fp * (qq - pp))) = (((fq * qq) - (fp * qq)) + (fp * (qq - pp))) by RLVECT_1: 35

              .= (((fq * qq) - (fp * qq)) + ((fp * qq) - (fp * pp))) by RLVECT_1: 34

              .= ((((fq * qq) - (fp * qq)) + (fp * qq)) - (fp * pp)) by RLVECT_1:def 3

              .= ((fq * qq) - (fp * pp)) by RLVECT_4: 1;

              then gqq in ( Ball (gpp,r0)) by A60, A67, A61;

              hence x in ( Ball (gp,r0)) by TOPREAL9: 13;

            end;

            hence thesis by A5;

          end;

            suppose

             A68: m > 0 ;

            set G1 = ].(fp - ((r0 / 2) / m)), (fp + ((r0 / 2) / m)).[;

            reconsider G1 as open Subset of R^1 by JORDAN6: 35, TOPMETR: 17, XXREAL_1: 225;



             A69: ( 0 + fp) < (((r0 / 2) / m) + fp) by A68, A4, XREAL_1: 6;

            (( - ((r0 / 2) / m)) + fp) < ( 0 + fp) by A68, A4, XREAL_1: 6;

            then

            consider W1 be Subset of X such that

             A70: p in W1 and

             A71: W1 is open and

             A72: (f .: W1) c= G1 by A1, JGRAPH_2: 10, A69, XXREAL_1: 4;

            reconsider W3 = (W1 /\ W2) as Subset of X;

            take W3;

            thus p in W3 by A70, A46, XBOOLE_0:def 4;

            thus W3 is open by A71, A45;

            (g .: W3) c= ( Ball (gp,r0))

            proof

              let x be object;

              assume x in (g .: W3);

              then

              consider q be object such that

               A73: q in ( dom g) and

               A74: q in W3 and

               A75: (g . q) = x by FUNCT_1:def 6;

              reconsider q as Point of X by A73;



               A76: q in the carrier of X;

              ( [#] X) c= ( [#] ( TOP-REAL n)) by PRE_TOPC:def 4;

              then

              reconsider qq = q as Point of ( TOP-REAL n1);

              reconsider fq = (f . q) as Real;



               A77: x = (fq * qq) by A3, A75;

              then

              reconsider gq = x as Point of ( Euclid n) by TOPREAL3: 8;

              reconsider gpp = gp as Point of ( TOP-REAL n1);

              reconsider gqq = gq as Point of ( TOP-REAL n1) by A77;



               A78: gpp = (fp * pp) by A3;

              reconsider r2 = (fq - fp) as Real;

              reconsider r3 = fp as Real;



               A79: ( |.(fq - fp).| * |.qq.|) = ( |.r2.| * |.qq.|)

              .= |.((fq - fp) * qq).| by TOPRNS_1: 7;



               A80: q in ( dom f) by A76, FUNCT_2:def 1;

              q in W1 by A74, XBOOLE_0:def 4;

              then (f . q) in (f .: W1) by A80, FUNCT_1:def 6;

              then ( |.(fq - fp).| * m) < (((r0 / 2) / m) * m) by A68, XREAL_1: 68, A72, RCOMP_1: 1;

              then ( |.(fq - fp).| * m) < ((r0 / 2) / (m / m)) by XCMPLX_1: 82;

              then

               A81: ( |.(fq - fp).| * m) < ((r0 / 2) / 1) by A68, XCMPLX_1: 60;

              qq in W2 by A74, XBOOLE_0:def 4;

              then |.qq.| in WW2;

              then |.qq.| <= m by XXREAL_2: 4;

              then ( |.qq.| * |.(fq - fp).|) <= (m * |.(fq - fp).|) by XREAL_1: 64;

              then

               A82: |.((fq - fp) * qq).| < (r0 / 2) by A79, A81, XXREAL_0: 2;



               A83: ( |.fp.| * |.(qq - pp).|) = ( |.r3.| * |.(qq - pp).|)

              .= |.(fp * (qq - pp)).| by TOPRNS_1: 7;

              qq in W2 by A74, XBOOLE_0:def 4;

              then qq in ( Ball (pp,((r0 / 2) / |.fp.|))) by XBOOLE_0:def 4;

              then ( |.fp.| * |.(qq - pp).|) < ( |.fp.| * ((r0 / 2) / |.fp.|)) by A44, XREAL_1: 68, TOPREAL9: 7;

              then ( |.fp.| * |.(qq - pp).|) < ((r0 / 2) / ( |.fp.| / |.fp.|)) by XCMPLX_1: 81;

              then

               A84: ( |.fp.| * |.(qq - pp).|) < ((r0 / 2) / 1) by A44, XCMPLX_1: 60;



               A85: ( |.((fq - fp) * qq).| + |.(fp * (qq - pp)).|) < ((r0 / 2) + (r0 / 2)) by A82, A84, A83, XREAL_1: 8;

               |.(((fq - fp) * qq) + (fp * (qq - pp))).| <= ( |.((fq - fp) * qq).| + |.(fp * (qq - pp)).|) by EUCLID_2: 52;

              then

               A86: |.(((fq - fp) * qq) + (fp * (qq - pp))).| < r0 by A85, XXREAL_0: 2;

              (((fq - fp) * qq) + (fp * (qq - pp))) = (((fq * qq) - (fp * qq)) + (fp * (qq - pp))) by RLVECT_1: 35

              .= (((fq * qq) - (fp * qq)) + ((fp * qq) - (fp * pp))) by RLVECT_1: 34

              .= ((((fq * qq) - (fp * qq)) + (fp * qq)) - (fp * pp)) by RLVECT_1:def 3

              .= ((fq * qq) - (fp * pp)) by RLVECT_4: 1;

              then gqq in ( Ball (gpp,r0)) by A77, A78, A86;

              hence x in ( Ball (gp,r0)) by TOPREAL9: 13;

            end;

            hence thesis by A5;

          end;

        end;

      end;

      hence thesis by A3, JGRAPH_2: 10;

    end;

    definition

      let n;

      let S be Subset of ( TOP-REAL n);

      :: MFOLD_1:def1

      attr S is ball means

      : Def1: ex p be Point of ( TOP-REAL n), r be Real st S = ( Ball (p,r));

    end

    registration

      let n;

      cluster ball for Subset of ( TOP-REAL n);

      correctness

      proof

        take ( Ball ( the Point of ( TOP-REAL n), the Real));

        thus thesis;

      end;

      cluster ball -> open for Subset of ( TOP-REAL n);

      correctness ;

    end

    registration

      let n;

      cluster non empty ball for 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;

    theorem :: MFOLD_1:3



     Th3: for S be open Subset of ( TOP-REAL n) st p in S holds ex B be 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 2;

      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 4;

      reconsider r as positive Real by A4;

      reconsider n1 = n as Element of NAT by ORDINAL1:def 12;

      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: 1;

    end;

    definition

      ::$Canceled

    end

    definition

      let n;

      :: MFOLD_1:def3

      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 ;

    end

    ::$Canceled

    theorem :: MFOLD_1:5



     Th5: n <> 0 & p is Point of ( Tunit_ball n) implies |.p.| < 1

    proof

      reconsider j = 1 as Real;

      assume n <> 0 ;

      then

      reconsider n1 = n as non zero Element of NAT by ORDINAL1:def 12;

      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 MFOLD_0: 2;

      hence thesis by TOPREAL9: 10;

    end;

    theorem :: MFOLD_1:6



     Th6: for f be Function of ( Tunit_ball n), ( TOP-REAL n) st n <> 0 & for a be Point of ( Tunit_ball n), b be Point of ( TOP-REAL n) st a = b holds (f . a) = ((1 / (1 - ( |.b.| * |.b.|))) * b) holds f is being_homeomorphism

    proof

      let f be Function of ( Tunit_ball n), ( TOP-REAL n) such that

       A1: n <> 0 and

       A2: for a be Point of ( Tunit_ball n), b be 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 4;

      reconsider n1 = n as non zero Element of NAT by A1, ORDINAL1:def 12;

      for y be object st y in ( [#] ( TOP-REAL n1)) holds ex x be object st [x, y] in f

      proof

        let y be object;

        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: 13;

          then x in ( Ball (( 0. ( TOP-REAL n)),1));

          then

           A6: x in ( dom f) by A3, MFOLD_0: 2;

          take x;

          (f . x) = ((1 / (1 - ( |.x.| * |.x.|))) * x) by A6, A2

          .= py by A5, RLVECT_1:def 8;

          hence [x, y] in f by A6, FUNCT_1:def 2;

        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 2;



           A9: |.x.| = ( |.r.| * |.py.|) by TOPRNS_1: 7

          .= (r * |.py.|) by A8, ABSVALUE:def 1;

           |.x.| < 1

          proof

            (( |.py.| * 4) + (1 + (4 * p2))) > ( 0 + (1 + (4 * p2))) by A7, XREAL_1: 6;

            then ( sqrt ((1 + (2 * |.py.|)) ^2 )) > ( sqrt (1 + (4 * p2))) by SQUARE_1: 27;

            then (1 + (2 * |.py.|)) > ( sqrt (1 + (4 * p2))) by SQUARE_1: 22;

            then ((1 + (2 * |.py.|)) - ( sqrt (1 + (4 * p2)))) > (( sqrt (1 + (4 * p2))) - ( sqrt (1 + (4 * p2)))) by XREAL_1: 9;

            then (((1 - ( sqrt (1 + (4 * p2)))) + (2 * |.py.|)) - (2 * |.py.|)) > ( 0 - (2 * |.py.|)) by XREAL_1: 9;

            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 2;

            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: 24;

            then (((2 * |.py.|) * ((2 * |.py.|) / (1 + ( sqrt (1 + (4 * p2)))))) / (2 * |.py.|)) < ((2 * |.py.|) / (2 * |.py.|)) by A7, XREAL_1: 74;

            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: 77;

            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: 13;

          then x in ( Ball (( 0. ( TOP-REAL n1)),1));

          then

           A10: x in ( dom f) by A3, MFOLD_0: 2;

          take x;



           A11: ( sqrt (1 + (4 * p2))) >= 0 by SQUARE_1:def 2;



           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 2;

            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: 76

          .= ((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 2

          .= ((4 / (2 * ((1 + ( sqrt (1 + (4 * p2)))) + (2 * p2)))) * p2)

          .= (((4 / 2) / ((1 + ( sqrt (1 + (4 * p2)))) + (2 * p2))) * p2) by XCMPLX_1: 78

          .= ((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: 76

          .= ((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 2

          .= (( - (4 * p2)) / (((1 + (2 * p2)) - ((2 * p2) * ( sqrt (1 + (4 * p2))))) - (1 + (4 * p2)))) by SQUARE_1:def 2

          .= (( - (4 * p2)) / (( - (2 * p2)) * (1 + ( sqrt (1 + (4 * p2))))))

          .= (((2 * ( - (2 * p2))) / ( - (2 * p2))) / (1 + ( sqrt (1 + (4 * p2))))) by XCMPLX_1: 78

          .= ((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, RLVECT_1:def 7

          .= (1 * py) by A8, XCMPLX_1: 60

          .= py by RLVECT_1:def 8;

          hence [x, y] in f by A10, FUNCT_1:def 2;

        end;

      end;

      then

       A14: ( rng f) = ( [#] ( TOP-REAL n1)) by RELSET_1: 10;

      for x1,x2 be object st x1 in ( dom f) & x2 in ( dom f) & (f . x1) = (f . x2) holds x1 = x2

      proof

        let x1,x2 be object;



         A15: ( [#] ( Tunit_ball n)) c= ( [#] ( TOP-REAL n)) by PRE_TOPC:def 4;

        assume

         A16: x1 in ( dom f);

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

        reconsider px2 = x2 as Point of ( TOP-REAL n1) by A17, 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 ((1 / (1 - ( |.px2.| * |.px2.|))) * px2) = ( 0. ( TOP-REAL n)) by A20, RLVECT_1: 10, EUCLID_2: 42;

          per cases by RLVECT_1: 11;

            suppose (1 / (1 - ( |.px2.| * |.px2.|))) = 0 ;

            then (1 - ( |.px2.| * |.px2.|)) = 0 ;

            then ( sqrt ( |.px2.| ^2 )) = 1 by SQUARE_1: 18;

            then

             A22: |.px2.| = 1 by SQUARE_1: 22;

            px2 in ( Ball (( 0. ( TOP-REAL n)),1)) by A18, MFOLD_0: 2;

            then

            consider p2 be Point of ( TOP-REAL n) such that

             A23: p2 = px2 & |.(p2 - ( 0. ( TOP-REAL n))).| < 1;

            thus thesis by A22, A23, RLVECT_1: 13;

          end;

            suppose px2 = ( 0. ( TOP-REAL n));

            hence thesis by A21, EUCLID_2: 42;

          end;

        end;

          suppose

           A24: |.px1.| <> 0 ;

          then ( |.px1.| * |.px1.|) < (1 * |.px1.|) by A16, Th5, XREAL_1: 68;

          then ( |.px1.| * |.px1.|) < 1 by A16, Th5, XXREAL_0: 2;

          then ( - ( |.px1.| * |.px1.|)) > ( - 1) by XREAL_1: 24;

          then

           A25: (( - ( |.px1.| * |.px1.|)) + 1) > (( - 1) + 1) by XREAL_1: 6;



           A26: px1 = (1 * px1) by RLVECT_1:def 8

          .= (((1 - ( |.px1.| * |.px1.|)) / (1 - ( |.px1.| * |.px1.|))) * px1) by A25, XCMPLX_1: 60

          .= ((1 - ( |.px1.| * |.px1.|)) * ((1 / (1 - ( |.px1.| * |.px1.|))) * px1)) by RLVECT_1:def 7

          .= (((1 - ( |.px1.| * |.px1.|)) / (1 - ( |.px2.| * |.px2.|))) * px2) by A20, RLVECT_1:def 7;



           A27: px2 <> ( 0. ( TOP-REAL n1))

          proof

            assume px2 = ( 0. ( TOP-REAL n1));

            then px1 = ( 0. ( TOP-REAL n1)) by A26, RLVECT_1: 10;

            hence contradiction by A24, TOPRNS_1: 23;

          end;

          then

           A28: |.px2.| <> 0 by EUCLID_2: 42;

          px2 in ( Ball (( 0. ( TOP-REAL n)),1)) by A18, MFOLD_0: 2;

          then

          consider p2 be Point of ( TOP-REAL n) such that

           A29: p2 = px2 & |.(p2 - ( 0. ( TOP-REAL n))).| < 1;



           A30: |.px2.| < 1 by A29, RLVECT_1: 13;

          then ( |.px2.| * |.px2.|) < (1 * |.px2.|) by A28, XREAL_1: 68;

          then ( |.px2.| * |.px2.|) < 1 by A30, XXREAL_0: 2;

          then ( - ( |.px2.| * |.px2.|)) > ( - 1) by XREAL_1: 24;

          then

           A31: (( - ( |.px2.| * |.px2.|)) + 1) > (( - 1) + 1) by XREAL_1: 6;

          set l = ((1 - ( |.px1.| * |.px1.|)) / (1 - ( |.px2.| * |.px2.|)));

          ((1 / (1 - ( |.px2.| * |.px2.|))) * px2) = (((1 / (1 - ( |.px1.| * |.px1.|))) * l) * px2) by A26, A20, RLVECT_1:def 7;

          then (((1 / (1 - ( |.px2.| * |.px2.|))) * px2) - (((1 / (1 - ( |.px1.| * |.px1.|))) * l) * px2)) = ( 0. ( TOP-REAL n)) by RLVECT_1: 5;

          then (((1 / (1 - ( |.px2.| * |.px2.|))) * px2) + (( - ((1 / (1 - ( |.px1.| * |.px1.|))) * l)) * px2)) = ( 0. ( TOP-REAL n)) by RLVECT_1: 79;

          then

           A32: (((1 / (1 - ( |.px2.| * |.px2.|))) + ( - ((1 / (1 - ( |.px1.| * |.px1.|))) * l))) * px2) = ( 0. ( TOP-REAL n)) by RLVECT_1:def 6;



           A33: (l * l) = ( |.l.| * |.l.|)

          proof

            per cases by ABSVALUE: 1;

              suppose |.l.| = l;

              hence thesis;

            end;

              suppose |.l.| = ( - l);

              hence thesis;

            end;

          end;

          ((1 / (1 - ( |.px2.| * |.px2.|))) + ( - ((1 / (1 - ( |.px1.| * |.px1.|))) * l))) = 0 by A27, A32, RLVECT_1: 11;



          then (1 / (1 - ( |.px2.| * |.px2.|))) = ((1 * l) / (1 - ( |.px1.| * |.px1.|)))

          .= (1 / ((1 - ( |.px1.| * |.px1.|)) / l)) by XCMPLX_1: 77;

          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: 81

          .= ((1 - ( |.px1.| * |.px1.|)) / 1) by A25, A31, XCMPLX_1: 60

          .= (1 - (( |.l.| * |.px2.|) * |.(l * px2).|)) by A26, TOPRNS_1: 7

          .= (1 - (( |.l.| * |.px2.|) * ( |.l.| * |.px2.|))) by TOPRNS_1: 7

          .= (1 - ((( |.l.| * |.l.|) * |.px2.|) * |.px2.|))

          .= (1 - (((l * l) * |.px2.|) * |.px2.|)) by A33;

          then ((1 + ((l * |.px2.|) * |.px2.|)) * (1 - l)) = 0 ;

          then (1 - l) = 0 by A25, A31;

          hence x1 = x2 by A26, RLVECT_1:def 8;

        end;

      end;

      then

       A34: f is one-to-one;

      consider f0 be Function of ( TOP-REAL n1), R^1 such that

       A35: (for p be Point of ( TOP-REAL n1) holds (f0 . p) = 1) & f0 is continuous by JGRAPH_2: 20;

      consider f1 be Function of ( TOP-REAL n1), R^1 such that

       A36: (for p be Point of ( TOP-REAL n1) holds (f1 . p) = |.p.|) & f1 is continuous by JORDAN2C: 84;

      consider f2 be Function of ( TOP-REAL n), R^1 such that

       A37: (for p be Point of ( TOP-REAL n), r1 be Real st (f1 . p) = r1 holds (f2 . p) = (r1 * r1)) & f2 is continuous by A36, JGRAPH_2: 22;

      consider f3 be Function of ( TOP-REAL n), R^1 such that

       A38: (for p be Point of ( TOP-REAL n), r1,r2 be Real st (f0 . p) = r1 & (f2 . p) = r2 holds (f3 . p) = (r1 - r2)) & f3 is continuous by A35, A37, JGRAPH_2: 21;

      reconsider f3 as continuous Function of ( TOP-REAL n), R^1 by A38;



       A39: for p be 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 A38

        .= (1 - (f2 . p)) by A35

        .= (1 - ((f1 . p) * (f1 . p))) by A37

        .= (1 - ( |.p.| * (f1 . p))) by A36

        .= (1 - ( |.p.| * |.p.|)) by A36;

      end;

      set f4 = (f3 | ( Tunit_ball n));

      for p be Point of ( Tunit_ball n) holds (f4 . p) <> 0

      proof

        let p be Point of ( Tunit_ball n);

        assume (f4 . p) = 0 ;

        then

         A40: (f3 . p) = 0 by FUNCT_1: 49;

        reconsider p1 = p as Point of ( TOP-REAL n1) by A4;



         A41: (1 - ( |.p1.| * |.p1.|)) = 0 by A40, A39;

        per cases ;

          suppose |.p1.| = 0 ;

          hence contradiction by A41;

        end;

          suppose |.p1.| <> 0 ;

          then ( |.p1.| * |.p1.|) < (1 * |.p1.|) by Th5, XREAL_1: 68;

          hence contradiction by A41, Th5;

        end;

      end;

      then

      consider f5 be Function of ( Tunit_ball n), R^1 such that

       A42: (for p be Point of ( Tunit_ball n), r1 be Real st (f4 . p) = r1 holds (f5 . p) = (1 / r1)) & f5 is continuous by JGRAPH_2: 26;

      consider f6 be Function of ( Tunit_ball n), ( TOP-REAL n) such that

       A43: (for a be Point of ( Tunit_ball n), b be Point of ( TOP-REAL n), r be Real st a = b & (f5 . a) = r holds (f6 . b) = (r * b)) & f6 is continuous by A42, Th2;



       A44: ( dom f) = the carrier of ( Tunit_ball n) by FUNCT_2:def 1

      .= ( dom f6) by FUNCT_2:def 1;

      for x be object st x in ( dom f) holds (f . x) = (f6 . x)

      proof

        let x be object;

        assume

         A45: x in ( dom f);

        then

        reconsider p1 = x as Point of ( Tunit_ball n);

        reconsider p = x as Point of ( TOP-REAL n) by A45, A4;

        (f4 . p) = (f3 . p) by A45, FUNCT_1: 49

        .= (1 - ( |.p.| * |.p.|)) by A39;

        then (f5 . p1) = (1 / (1 - ( |.p.| * |.p.|))) by A42;

        then (f6 . p1) = ((1 / (1 - ( |.p.| * |.p.|))) * p) by A43;

        hence (f . x) = (f6 . x) by A2;

      end;

      then

       A47: f = f6 by A44;

      consider f8 be Function of ( TOP-REAL n), R^1 such that

       A48: (for p be Point of ( TOP-REAL n), r1 be Real st (f2 . p) = r1 holds (f8 . p) = (4 * r1)) & f8 is continuous by A37, JGRAPH_2: 23;

      consider f9 be Function of ( TOP-REAL n), R^1 such that

       A49: (for p be Point of ( TOP-REAL n), r1,r2 be Real st (f0 . p) = r1 & (f8 . p) = r2 holds (f9 . p) = (r1 + r2)) & f9 is continuous by A48, A35, JGRAPH_2: 19;



       A50: for p be 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 A49

        .= (1 + (f8 . p)) by A35

        .= (1 + (4 * (f2 . p))) by A48

        .= (1 + (4 * ((f1 . p) * (f1 . p)))) by A37

        .= (1 + (4 * ((f1 . p) * |.p.|))) by A36

        .= (1 + (4 * ( |.p.| * |.p.|))) by A36

        .= (1 + ((4 * |.p.|) * |.p.|));

      end;



       A51: for p be Point of ( TOP-REAL n) holds ex r be Real 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 A50;

      end;

      consider f10 be Function of ( TOP-REAL n), R^1 such that

       A52: (for p be Point of ( TOP-REAL n), r1 be Real st (f9 . p) = r1 holds (f10 . p) = ( sqrt r1)) & f10 is continuous by A51, A49, JGRAPH_3: 5;

      consider f11 be Function of ( TOP-REAL n), R^1 such that

       A53: (for p be Point of ( TOP-REAL n), r1,r2 be Real st (f0 . p) = r1 & (f10 . p) = r2 holds (f11 . p) = (r1 + r2)) & f11 is continuous by A52, A35, JGRAPH_2: 19;

      for p be Point of ( TOP-REAL n) holds (f11 . p) <> 0

      proof

        let p be Point of ( TOP-REAL n);



         A54: (f11 . p) = ((f0 . p) + (f10 . p)) by A53

        .= (1 + (f10 . p)) by A35

        .= (1 + ( sqrt (f9 . p))) by A52;

        consider r be Real such that

         A55: r = (f9 . p) & r >= 0 by A51;

        ( sqrt (f9 . p)) >= 0 by A55, SQUARE_1:def 2;

        hence thesis by A54;

      end;

      then

      consider f12 be Function of ( TOP-REAL n), R^1 such that

       A56: (for p be Point of ( TOP-REAL n), r1 be Real st (f11 . p) = r1 holds (f12 . p) = (1 / r1)) & f12 is continuous by A53, JGRAPH_2: 26;

      consider f13 be Function of ( TOP-REAL n), R^1 such that

       A57: (for p be Point of ( TOP-REAL n), r1 be Real st (f12 . p) = r1 holds (f13 . p) = (2 * r1)) & f13 is continuous by A56, JGRAPH_2: 23;



       A58: for p be 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 A57

        .= (2 * (1 / (f11 . p))) by A56

        .= (2 / ((f0 . p) + (f10 . p))) by A53

        .= (2 / ((f0 . p) + ( sqrt (f9 . p)))) by A52

        .= (2 / (1 + ( sqrt (f9 . p)))) by A35

        .= (2 / (1 + ( sqrt (1 + ((4 * |.p.|) * |.p.|))))) by A50;

      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

       A59: (for a be Point of X, b be Point of ( TOP-REAL n), r be Real st a = b & (f13 . a) = r holds (f14 . b) = (r * b)) & f14 is continuous by A57, Th2;

      reconsider f14 as continuous Function of ( TOP-REAL n), ( TOP-REAL n) by A59;



       A60: ( dom f14) = the carrier of ( TOP-REAL n) by FUNCT_2:def 1;



       A61: for r be Real holds ( |.r.| * |.r.|) = (r * r)

      proof

        let r be Real;

        per cases by ABSVALUE: 1;

          suppose |.r.| = r;

          hence thesis;

        end;

          suppose |.r.| = ( - r);

          hence thesis;

        end;

      end;

      for y be object holds y in the carrier of ( Tunit_ball n) iff ex x be object st x in ( dom f14) & y = (f14 . x)

      proof

        let y be object;

        hereby

          assume

           A62: y in the carrier of ( Tunit_ball n);

          ( [#] ( Tunit_ball n)) c= ( [#] ( TOP-REAL n)) by PRE_TOPC:def 4;

          then

          reconsider q = y as Point of ( TOP-REAL n1) by A62;

           |.q.| < 1 by A62, Th5;

          then ( |.q.| * |.q.|) <= (1 * |.q.|) by XREAL_1: 64;

          then ( |.q.| * |.q.|) < 1 by A62, Th5, XXREAL_0: 2;

          then

           A63: 0 < (1 - ( |.q.| * |.q.|)) by XREAL_1: 50;

          set p = ((1 / (1 - ( |.q.| * |.q.|))) * q);

           |.p.| = ( |.(1 / (1 - ( |.q.| * |.q.|))).| * |.q.|) by TOPRNS_1: 7;



          then ( |.p.| * |.p.|) = ((( |.(1 / (1 - ( |.q.| * |.q.|))).| * |.(1 / (1 - ( |.q.| * |.q.|))).|) * |.q.|) * |.q.|)

          .= ((((1 / (1 - ( |.q.| * |.q.|))) * (1 / (1 - ( |.q.| * |.q.|)))) * |.q.|) * |.q.|) by A61

          .= ((((1 * 1) / ((1 - ( |.q.| * |.q.|)) * (1 - ( |.q.| * |.q.|)))) * |.q.|) * |.q.|) by XCMPLX_1: 76

          .= (( |.q.| * |.q.|) / ((1 - ( |.q.| * |.q.|)) * (1 - ( |.q.| * |.q.|))));



          then

           A64: (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 A63, 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: 76;

          ( sqrt (1 + ((4 * |.p.|) * |.p.|))) = ((1 + ( |.q.| * |.q.|)) / (1 - ( |.q.| * |.q.|))) by A63, A64, SQUARE_1: 22;



          then

           A65: (1 + ( sqrt (1 + ((4 * |.p.|) * |.p.|)))) = (((1 - ( |.q.| * |.q.|)) / (1 - ( |.q.| * |.q.|))) + ((1 + ( |.q.| * |.q.|)) / (1 - ( |.q.| * |.q.|)))) by A63, XCMPLX_1: 60

          .= (2 / (1 - ( |.q.| * |.q.|)));

          reconsider x = p as object;

          take x;

          thus x in ( dom f14) by A60;



          thus (f14 . x) = ((f13 . p) * p) by A59

          .= ((2 / (2 / (1 - ( |.q.| * |.q.|)))) * p) by A65, A58

          .= ((1 - ( |.q.| * |.q.|)) * p) by XCMPLX_1: 52

          .= (((1 - ( |.q.| * |.q.|)) / (1 - ( |.q.| * |.q.|))) * q) by RLVECT_1:def 7

          .= (1 * q) by A63, XCMPLX_1: 60

          .= y by RLVECT_1:def 8;

        end;

        given x be object such that

         A66: x in ( dom f14) & y = (f14 . x);

        reconsider p = x as Point of ( TOP-REAL n1) by A66;

        y in ( rng f14) by A66, FUNCT_1: 3;

        then

        reconsider q = y as Point of ( TOP-REAL n1);

        y = ((f13 . p) * p) by A59, A66

        .= ((2 / (1 + ( sqrt (1 + ((4 * |.p.|) * |.p.|))))) * p) by A58;

        then |.q.| = ( |.(2 / (1 + ( sqrt (1 + ((4 * |.p.|) * |.p.|))))).| * |.p.|) by TOPRNS_1: 7;



        then

         A67: ( |.q.| * |.q.|) = ((( |.(2 / (1 + ( sqrt (1 + ((4 * |.p.|) * |.p.|))))).| * |.(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 A61;

        ( |.q.| * |.q.|) < 1

        proof

          assume ( |.q.| * |.q.|) >= 1;

          then

           A68: ((((2 * 2) / ((1 + ( sqrt (1 + ((4 * |.p.|) * |.p.|)))) * (1 + ( sqrt (1 + ((4 * |.p.|) * |.p.|)))))) * |.p.|) * |.p.|) >= 1 by A67, XCMPLX_1: 76;

           0 <= ( sqrt (1 + ((4 * |.p.|) * |.p.|))) by SQUARE_1:def 2;

          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 A68, XREAL_1: 64;

          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 2;

          then (((4 * |.p.|) * |.p.|) - ((4 * |.p.|) * |.p.|)) >= (((2 + (2 * ( sqrt (1 + ((4 * |.p.|) * |.p.|))))) + ((4 * |.p.|) * |.p.|)) - ((4 * |.p.|) * |.p.|)) by XREAL_1: 9;

          then ( 0 / 2) > ((2 * ( sqrt (1 + ((4 * |.p.|) * |.p.|)))) / 2);

          hence contradiction by SQUARE_1:def 2;

        end;

        then ( |.q.| ^2 ) < 1;

        then

         A69: |.q.| < 1 by SQUARE_1: 52;

         |.(q + ( - ( 0. ( TOP-REAL n1)))).| <= ( |.q.| + |.( - ( 0. ( TOP-REAL n1))).|) by EUCLID_2: 52;

        then |.(q + ( - ( 0. ( TOP-REAL n1)))).| <= ( |.q.| + |.( 0. ( TOP-REAL n1)).|) by JGRAPH_5: 10;

        then |.(q + ( - ( 0. ( TOP-REAL n1)))).| <= ( |.q.| + 0 ) by EUCLID_2: 39;

        then |.(q - ( 0. ( TOP-REAL n1))).| < 1 by A69, 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 5;

        hence y in the carrier of ( Tunit_ball n);

      end;

      then

       A70: ( rng f14) = the carrier of ( Tunit_ball n) by FUNCT_1:def 3;

      then

      reconsider f14 as Function of ( TOP-REAL n), ( Tunit_ball n) by A60, FUNCT_2: 1;



       A71: ( dom f14) = the carrier of ( TOP-REAL n) by FUNCT_2:def 1

      .= ( dom (f " )) by FUNCT_2:def 1;

      for x be object st x in ( dom f14) holds (f14 . x) = ((f " ) . x)

      proof

        let x be object;

        assume

         A72: x in ( dom f14);

        reconsider g = f as Function;

        f is onto by A14, FUNCT_2:def 3;

        then

         A73: (f " ) = (g " ) by A34, TOPS_2:def 4;



         A74: (f14 . x) in ( rng f14) by A72, FUNCT_1: 3;

        then

         A75: (f14 . x) in ( dom f) by A70, FUNCT_2:def 1;

        reconsider p = x as Point of ( TOP-REAL n1) by A72;



         A76: (f14 . p) = ((f13 . p) * p) by A59

        .= ((2 / (1 + ( sqrt (1 + ((4 * |.p.|) * |.p.|))))) * p) by A58;

        reconsider y = (f14 . x) as Point of ( Tunit_ball n) by A74;

        reconsider q = y as Point of ( TOP-REAL n1) by A4;



         A77: 0 <= ( sqrt (1 + ((4 * |.p.|) * |.p.|))) by SQUARE_1:def 2;

         |.q.| = ( |.(2 / (1 + ( sqrt (1 + ((4 * |.p.|) * |.p.|))))).| * |.p.|) by A76, TOPRNS_1: 7;



        then ( |.q.| * |.q.|) = ((( |.(2 / (1 + ( sqrt (1 + ((4 * |.p.|) * |.p.|))))).| * |.(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 A61

        .= ((((2 * 2) / ((1 + ( sqrt (1 + ((4 * |.p.|) * |.p.|)))) * (1 + ( sqrt (1 + ((4 * |.p.|) * |.p.|)))))) * |.p.|) * |.p.|) by XCMPLX_1: 76

        .= (((4 * |.p.|) * |.p.|) / ((1 + ( sqrt (1 + ((4 * |.p.|) * |.p.|)))) ^2 ));



        then

         A78: (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 A77, 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 2

        .= ((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 A77, XCMPLX_1: 91;

        (f . (f14 . x)) = ((1 / (2 / (1 + ( sqrt (1 + ((4 * |.p.|) * |.p.|)))))) * q) by A2, A78

        .= (((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 A76, RLVECT_1:def 7

        .= (((2 * (1 + ( sqrt (1 + ((4 * |.p.|) * |.p.|))))) / (2 * (1 + ( sqrt (1 + ((4 * |.p.|) * |.p.|)))))) * p) by XCMPLX_1: 76

        .= (1 * p) by A77, XCMPLX_1: 60

        .= p by RLVECT_1:def 8;

        then [(f14 . x), x] in f by A75, FUNCT_1:def 2;

        then [x, (f14 . x)] in (g ~ ) by RELAT_1:def 7;

        then [x, (f14 . x)] in (g " ) by A34, FUNCT_1:def 5;

        hence (f14 . x) = ((f " ) . x) by A73, FUNCT_1: 1;

      end;

      then (f " ) is continuous by A71, FUNCT_1: 2, PRE_TOPC: 27;

      hence thesis by A3, A14, A34, A43, A47, TOPS_2:def 5;

    end;

    theorem :: MFOLD_1:7

    for r be positive Real, f be Function of ( Tunit_ball n), ( Tball (p,r)) st n <> 0 & for a be Point of ( Tunit_ball n), b be 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, f be Function of ( Tunit_ball n), ( Tball (p,r)) such that

       A1: n <> 0 and

       A2: for a be Point of ( Tunit_ball n), b be Point of ( TOP-REAL n) st a = b holds (f . a) = ((r * b) + p);

      reconsider n1 = n as non zero Element of NAT by A1, ORDINAL1:def 12;

      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 be Point of ( TOP-REAL n1) holds ex y be Point of ( TOP-REAL n1) st P[u, y];

      consider F be Function of ( TOP-REAL n1), ( TOP-REAL n1) such that

       A4: for x be 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 be Point of ( TOP-REAL n1) holds ex y be Point of ( TOP-REAL n1) st R[u, y];

      consider G be Function of ( TOP-REAL n1), ( TOP-REAL n1) such that

       A6: for a be 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: 62;

      for p be 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)))

        .= (((1 / r) * p) + (( - (1 / r)) * x)) by FUNCOP_1: 7

        .= (((1 / r) * p) - ((1 / r) * x)) by RLVECT_1: 79

        .= ((1 / r) * (p - x)) by RLVECT_1: 34

        .= (G . p) by A6;

      end;

      then

       A8: G is continuous by TOPALG_1: 16;



       A9: ( dom f) = ( [#] U) by FUNCT_2:def 1;



       A10: ( dom f) = the carrier of U by FUNCT_2:def 1;

      for p be 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 RLVECT_1:def 8

        .= ((r * p) + (f2 . p))

        .= ((r * p) + x) by FUNCOP_1: 7

        .= (F . p) by A4;

      end;

      then

       A11: F is continuous by TOPALG_1: 16;



       A12: the carrier of B = ( Ball (x,r)) by MFOLD_0: 2;



       A13: the carrier of U = ( Ball (( 0. ( TOP-REAL n)),1)) by MFOLD_0: 2;



       A14: for a be object st a in ( dom f) holds (f . a) = ((F | ( Ball (( 0. ( TOP-REAL n)),1))) . a)

      proof

        let a be object such that

         A15: a in ( dom f);

        reconsider y = a as Point of ( TOP-REAL n1) by A15, PRE_TOPC: 25;



        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: 49;

      end;



       A16: ((1 / r) * r) = 1 by XCMPLX_1: 87;



       A17: ( rng f) = ( [#] B)

      proof

        now

          let b be object;

          assume

           A18: b in ( [#] B);

          then

          reconsider c = b as Point of ( TOP-REAL n1) by PRE_TOPC: 25;

          reconsider r1 = (1 / r) as Real;

          set a = (r1 * (c - x));



           A19: |.(a - ( 0. ( TOP-REAL n1))).| = |.a.| by RLVECT_1: 13

          .= ( |.r1.| * |.(c - x).|) by TOPRNS_1: 7

          .= (r1 * |.(c - x).|) by ABSVALUE:def 1;

          ((1 / r) * |.(c - x).|) < ((1 / r) * r) by XREAL_1: 68, A12, A18, TOPREAL9: 7;

          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 RLVECT_1:def 7

          .= ((c - x) + x) by A16, RLVECT_1:def 8

          .= b by RLVECT_4: 1;

          hence b in ( rng f) by A13, A10, A20, FUNCT_1:def 3;

        end;

        then ( [#] B) c= ( rng f);

        hence thesis by XBOOLE_0:def 10;

      end;

      now

        let a,b be object 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, RLVECT_4: 1;

        hence a = b by RLVECT_1: 36, RLVECT_4: 1;

      end;

      then

       A25: f is one-to-one;



       A26: for a be object st a in ( dom (f " )) holds ((f " ) . a) = ((G | ( Ball (x,r))) . a)

      proof

        reconsider ff = f as Function;

        let a be object such that

         A27: a in ( dom (f " ));

        reconsider y = a as Point of ( TOP-REAL n1) by A27, PRE_TOPC: 25;

        reconsider r1 = (1 / r) as Real;

        set e = ((1 / r) * (y - x));



         A28: f is onto by A17, FUNCT_2:def 3;



         A29: |.(e - ( 0. ( TOP-REAL n1))).| = |.e.| by RLVECT_1: 13

        .= ( |.r1.| * |.(y - x).|) by TOPRNS_1: 7

        .= (r1 * |.(y - x).|) by ABSVALUE:def 1;

        ((1 / r) * |.(y - x).|) < ((1 / r) * r) by XREAL_1: 68, A27, A12, TOPREAL9: 7;

        then

         A30: ((1 / r) * (y - x)) in ( Ball (( 0. ( TOP-REAL n)),1)) by A16, A29;



        then (f . e) = ((r * e) + x) by A2, A13

        .= (((r * (1 / r)) * (y - x)) + x) by RLVECT_1:def 7

        .= ((y - x) + x) by A16, RLVECT_1:def 8

        .= y by RLVECT_4: 1;

        then ((ff " ) . a) = ((1 / r) * (y - x)) by A13, A10, A25, A30, FUNCT_1: 32;



        hence ((f " ) . a) = ((1 / r) * (y - x)) by A28, A25, TOPS_2:def 4

        .= (G . y) by A6

        .= ((G | ( Ball (x,r))) . a) by A12, A27, FUNCT_1: 49;

      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: 62;

      then

       A31: f is continuous by A13, A10, A11, A14, BORSUK_4: 44, FUNCT_1: 2;



       A32: ( dom (f " )) = the carrier of B by FUNCT_2:def 1;

      (f " ) is continuous by A32, A12, A7, A8, A26, BORSUK_4: 44, FUNCT_1: 2;

      hence thesis by A9, A17, A25, A31, TOPS_2:def 5;

    end;

    theorem :: MFOLD_1:8



     Th8: (( Tunit_ball n),( TOP-REAL n)) are_homeomorphic

    proof

      reconsider n1 = n as Element of NAT by ORDINAL1:def 12;

      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 be Point of ( TOP-REAL n1) st w = $1 & $2 = ((1 / (1 - ( |.w.| * |.w.|))) * w);



         A2: for u be Point of U holds ex y be 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: 25;

          set y = ((1 / (1 - ( |.v.| * |.v.|))) * v);

          reconsider y as Point of C;

          take y;

          thus thesis;

        end;

        consider f be Function of U, C such that

         A3: for x be Point of U holds P[x, (f . x)] from FUNCT_2:sch 3( A2);

        for a be Point of U, b be 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;

        hence thesis by T_0TOPSP:def 1, A1, Th6;

      end;

        suppose

         A4: n is empty;



         A5: for x be object holds x in ( Ball (( 0. ( TOP-REAL 0 )),1)) iff x = ( 0. ( TOP-REAL 0 ))

        proof

          let x be object;

          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: 39;

          hence x in ( Ball (( 0. ( TOP-REAL 0 )),1));

        end;

        ( [#] ( TOP-REAL 0 )) = {( 0. ( TOP-REAL 0 ))} by EUCLID: 22, EUCLID: 77

        .= ( Ball (( 0. ( TOP-REAL 0 )),1)) by A5, TARSKI:def 1;

        hence thesis by A4, MFOLD_0: 1;

      end;

    end;

    reserve q for Point of ( TOP-REAL n);

    ::$Canceled

    theorem :: MFOLD_1:10



     Th10: for B be 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 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 MFOLD_0: 1;



       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 MFOLD_0: 3;

      then (B1,( TOP-REAL n)) are_homeomorphic by A3, BORSUK_3: 3;

      hence (B,( [#] ( TOP-REAL n))) are_homeomorphic by A1, METRIZTS:def 1, A2, BORSUK_3: 3;

    end;

    theorem :: MFOLD_1:11



     Th11: for M,N be non empty TopSpace holds for p be Point of M, U be a_neighborhood of p, B be open Subset of N st (U,B) are_homeomorphic holds ex V be open Subset of M, S be 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

       A0: (U,B) are_homeomorphic ;

      then

       A1: ((M | U),(N | B)) are_homeomorphic by METRIZTS:def 1;

      consider f be Function of (M | U), (N | B) such that

       A2: f is being_homeomorphism by T_0TOPSP:def 1, A0, METRIZTS:def 1;

      consider V be Subset of M such that

       A3: V is open & V c= U & p in V by CONNSP_2: 6;

      V c= ( [#] (M | U)) by A3, PRE_TOPC:def 5;

      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: 18;

      reconsider f1 = f as Function of M1, N1;

      ( rng f) c= ( [#] (N | B));

      then

       A4: ( rng f) c= B by PRE_TOPC:def 5;



       A5: (((M | U) | V1),((N | B) | (f .: V1))) are_homeomorphic by METRIZTS:def 1, A2, METRIZTS: 3;

      reconsider V as open Subset of M by A3;

      B = the carrier of (N | B) by PRE_TOPC: 8;

      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 5;

      then

      reconsider S = (f .: V1) as Subset of N by XBOOLE_1: 1;

      reconsider S1 = (f .: V1) as Subset of N1;



       A6: for P be 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 2;

      V1 = (V /\ ( [#] M1)) by XBOOLE_1: 28;

      then V1 in the topology of M1 by A7, PRE_TOPC:def 4;

      then S1 is open by A6, PRE_TOPC:def 2;

      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: 7;

      (f .: U) c= ( rng f) by RELAT_1: 111;

      then

       A9: (f .: U) c= B by A4;

      (f .: V) c= (f .: U) by A3, RELAT_1: 123;

      then ((N | B) | (f .: V1)) = (N | S) by A9, PRE_TOPC: 7, XBOOLE_1: 1;

      hence (V,S) are_homeomorphic by A5, A8, METRIZTS:def 1;

    end;

    begin

    reserve M for non empty TopSpace;



     Lm1: (for p be Point of M holds ex U be a_neighborhood of p, S be open Subset of ( TOP-REAL n) st (U,S) are_homeomorphic ) implies for p be Point of M holds ex U be a_neighborhood of p, B be non empty ball Subset of ( TOP-REAL n) st (U,B) are_homeomorphic

    proof

      assume

       A1: for p be Point of M holds ex U be a_neighborhood of p, S be open Subset of ( TOP-REAL n) st (U,S) are_homeomorphic ;

      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;

      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;

      consider f be Function of (M | U1), (( TOP-REAL n) | S) such that

       A5: f is being_homeomorphism by T_0TOPSP:def 1, A3, METRIZTS:def 1;



       A6: p in ( [#] (M | U1)) by A3, PRE_TOPC:def 5;

      reconsider S1 = (( TOP-REAL n) | S) as non empty TopSpace by A4, YELLOW14: 18;

      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 5;



       A8: ( [#] (( TOP-REAL n) | S)) c= ( [#] ( TOP-REAL n)) by PRE_TOPC:def 4;

      (f . p) in the carrier of (( TOP-REAL n) | S) by A6, FUNCT_2: 5;

      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, A7, Th3, FUNCT_2: 5;

      reconsider B as non empty ball Subset of ( TOP-REAL n) by A9;



       A10: (f " ) is being_homeomorphism by A5, TOPS_2: 56;

      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: 49;

      then

       A14: ((f " ) . q) in ((f " ) .: B1) by A9, FUNCT_1:def 6;

      reconsider U2 = ((f " ) .: B1) as non empty Subset of M1 by A13;



       A15: ( dom ((f " ) | B1)) = B1 by A13, RELAT_1: 62;



       A16: ( dom ((f " ) | B1)) = ( [#] (S1 | B1)) by A15, PRE_TOPC:def 5

      .= the carrier of (S1 | B1);

      ( rng ((f " ) | B1)) = ((f " ) .: B1) by RELAT_1: 115

      .= ( [#] (M1 | U2)) by PRE_TOPC:def 5

      .= the carrier of (M1 | U2);

      then

      reconsider g = ((f " ) | B1) as Function of (S1 | B1), (M1 | U2) by A16, FUNCT_2: 1;



       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, A6, TOPS_2:def 5;

      f is onto by A11, FUNCT_2:def 3;

      then (f1 " ) = (f " ) by A12, TOPS_2:def 4;

      then

       A19: p1 in U2 by A14, A18, FUNCT_1: 34;



       A20: ( [#] M1) c= ( [#] M) by PRE_TOPC:def 4;

      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 2;

      B1 = (B /\ ( [#] S1)) by XBOOLE_1: 28;

      then B1 in the topology of S1 by A21, PRE_TOPC:def 4;

      then B1 is open by PRE_TOPC:def 2;

      then ((f " ) .: B1) is open by A10, TOPGRP_1: 25;

      then

      reconsider V as a_neighborhood of p by A19, CONNSP_2: 3, CONNSP_2: 9;

      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 5;

      ((f " ) .: B1) c= ( rng (f " )) by RELAT_1: 111;

      then

       A24: (M | V) = (M1 | U2) by A23, PRE_TOPC: 7, XBOOLE_1: 1;

      (S1 | B1) = (( TOP-REAL n) | B) by A9, PRE_TOPC: 7;

      hence (V,B) are_homeomorphic by A24, A22, METRIZTS:def 1;

    end;

    theorem :: MFOLD_1:12



     Def4: M is n -locally_euclidean without_boundary iff for p be Point of M holds ex U be a_neighborhood of p, S be open Subset of ( TOP-REAL n) st (U,S) are_homeomorphic

    proof

      set TRn = ( TOP-REAL n);

      hereby

        assume

         A1: M is n -locally_euclidean without_boundary;

        let p be Point of M;

        the carrier of M = ( Int M) by A1, MFOLD_0:def 6;

        then

        consider U be a_neighborhood of p, m be Nat such that

         A2: ((M | U),( Tball (( 0. ( TOP-REAL m)),1))) are_homeomorphic by MFOLD_0:def 4;

        set TR = ( TOP-REAL m);

        consider W be a_neighborhood of p such that

         A3: ((M | W),( Tdisk (( 0. TRn),1))) are_homeomorphic by A1, MFOLD_0:def 3;

        p in ( Int U) & p in ( Int W) by CONNSP_2:def 1;

        then n = m by A2, A3, BROUWER3: 15, XBOOLE_0: 3;

        hence ex U be a_neighborhood of p, S be open Subset of TRn st (U,S) are_homeomorphic by A2, METRIZTS:def 1;

      end;

      assume

       R: for p be Point of M holds ex U be a_neighborhood of p, S be open Subset of TRn st (U,S) are_homeomorphic ;



       K: for p be Point of M holds ex U be a_neighborhood of p st ((M | U),( Tball (( 0. TRn),1))) are_homeomorphic

      proof

        let p be Point of M;

        consider U be a_neighborhood of p, B be non empty ball Subset of TRn such that

         B1: (U,B) are_homeomorphic by R, Lm1;

        take U;

        consider q be Point of TRn, r be Real such that

         B2: B = ( Ball (q,r)) by Def1;



         B3: ((M | U),(TRn | ( Ball (q,r)))) are_homeomorphic by B1, B2, METRIZTS:def 1;

        p in ( Int U) by CONNSP_2:def 1;

        then

         B4: ex W be Subset of M st W is open & W c= U & p in W by TOPS_1: 22;

        r > 0 by B2;

        then (( Tball (q,r)),( Tball (( 0. TRn),1))) are_homeomorphic by MFOLD_0: 3;

        hence ((M | U),( Tball (( 0. TRn),1))) are_homeomorphic by B3, BORSUK_3: 3, B4, B2;

      end;

       ZZ:

      now

        let p be Point of M;

        ex U be a_neighborhood of p st ((M | U),( Tball (( 0. ( TOP-REAL n)),1))) are_homeomorphic by K;

        hence ex U be a_neighborhood of p, n st ((M | U),( Tball (( 0. ( TOP-REAL n)),1))) are_homeomorphic ;

      end;

      then

       F: M is without_boundary locally_euclidean by MFOLD_0: 6;

      for p be Point of M holds ex U be a_neighborhood of p st ((M | U),( Tdisk (( 0. ( TOP-REAL n)),1))) are_homeomorphic

      proof

        let p be Point of M;

        consider U be a_neighborhood of p, m be Nat such that

         B1: ((M | U),( Tdisk (( 0. ( TOP-REAL m)),1))) are_homeomorphic by MFOLD_0:def 2, F;

        consider W be a_neighborhood of p such that

         A3: ((M | W),( Tball (( 0. TRn),1))) are_homeomorphic by K;

        p in ( Int U) & p in ( Int W) by CONNSP_2:def 1;

        then n = m by B1, A3, BROUWER3: 15, XBOOLE_0: 3;

        hence thesis by B1;

      end;

      hence thesis by ZZ, MFOLD_0: 6, MFOLD_0:def 3;

    end;

    registration

      let n;

      cluster ( TOP-REAL n) -> without_boundaryn -locally_euclidean;

      coherence

      proof

        now

          let p be Point of ( TOP-REAL n);

          p in ( [#] ( TOP-REAL n));

          then p in ( Int ( [#] ( TOP-REAL n))) by TOPS_1: 15;

          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;

        hence thesis by Def4;

      end;

    end

    theorem :: MFOLD_1:13

    M is without_boundaryn -locally_euclidean iff for p be Point of M holds ex U be a_neighborhood of p, B be ball Subset of ( TOP-REAL n) st (U,B) are_homeomorphic

    proof

      hereby

        assume M is without_boundaryn -locally_euclidean;

        then

         AA: for p be Point of M holds ex U be a_neighborhood of p, S be open Subset of ( TOP-REAL n) st (U,S) are_homeomorphic by Def4;

        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 AA, 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 be Point of M holds ex U be a_neighborhood of p, B be 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 without_boundaryn -locally_euclidean by Def4;

    end;

    theorem :: MFOLD_1:14



     Th13: M is without_boundaryn -locally_euclidean iff for p be Point of M holds ex U be a_neighborhood of p st (U,( [#] ( TOP-REAL n))) are_homeomorphic

    proof

      hereby

        assume M is without_boundaryn -locally_euclidean;

        then

         AA: for p be Point of M holds ex U be a_neighborhood of p, S be open Subset of ( TOP-REAL n) st (U,S) are_homeomorphic by Def4;

        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 Lm1, AA;

        take U;



         A3: (( TOP-REAL n) | ( [#] ( TOP-REAL n))) = the TopStruct of ( TOP-REAL n) by TSEP_1: 93;

        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: 18;



         A4: (U1,B1) are_homeomorphic by A2, METRIZTS:def 1;

        (B1, the TopStruct of ( TOP-REAL n)) are_homeomorphic by Th10, A3, METRIZTS:def 1;

        hence (U,( [#] ( TOP-REAL n))) are_homeomorphic by A3, METRIZTS:def 1, A4, BORSUK_3: 3;

      end;

      assume

       A6: for p be Point of M holds ex U be 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);

        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: 93;



         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: 18;

        reconsider S1 = (( TOP-REAL n) | S) as non empty TopSpace;



         A11: ( the TopStruct of ( TOP-REAL n),S1) are_homeomorphic by Th10, 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 without_boundaryn -locally_euclidean by Def4;

    end;

    registration

      cluster without_boundary locally_euclidean -> first-countable for non empty TopSpace;

      correctness

      proof

        let M be non empty TopSpace;

        assume

         A1: M is without_boundary locally_euclidean;

        for p be Point of M holds ex B be Basis of p st B is countable

        proof

          let p be Point of M;

          consider U be a_neighborhood of p, n such that

           A2: ((M | U),( Tball (( 0. ( TOP-REAL n)),1))) are_homeomorphic by A1, MFOLD_0: 6;

          set TR = ( TOP-REAL n);

          p in ( Int U) by CONNSP_2:def 1;

          then

           K1: ex W be Subset of M st W is open & W c= U & p in W by TOPS_1: 22;

          ( Ball (( 0. TR),1)) is non empty ball;

          then (( Tball (( 0. TR),1)),(TR | ( [#] TR))) are_homeomorphic by Th10, METRIZTS:def 1;

          then ((M | U),(TR | ( [#] TR))) are_homeomorphic by A2, K1, BORSUK_3: 3;

          then ((M | U), the TopStruct of TR) are_homeomorphic by TSEP_1: 93;

          then

          consider f be Function of (M | U), the TopStruct of TR such that

           A3: f is being_homeomorphism by T_0TOPSP:def 1;



           A4: ( dom f) = ( [#] (M | U)) & ( rng f) = ( [#] the TopStruct of TR) & 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 5;



           A6: f is onto by A4, FUNCT_2:def 3;



           A7: ( Int U) c= U by TOPS_1: 16;



           A8: p in ( Int U) by CONNSP_2:def 1;



           A9: p in ( dom f) by CONNSP_2:def 1, A7, A5;

          (f . p) in ( rng f) by A8, A7, A5, FUNCT_1: 3;

          then

          reconsider q = (f . p) as Point of ( TOP-REAL n);

          reconsider n1 = n as Element of NAT by ORDINAL1:def 12;

          consider B1 be Basis of q such that

           A10: 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 be Element of A : X in B1 };



           A11: ( card B1) c= omega by A10, CARD_3:def 14;

          ( card B) c= ( card B1) from TREES_2:sch 2;

          then

           A12: ( card B) c= omega by A11;

          for x be object st x in B holds x in ( bool the carrier of M)

          proof

            let x be object;

            assume x in B;

            then

            consider X1 be Element of A such that

             A13: x = F(X1) & X1 in B1;

            thus x in ( bool the carrier of M) by A13;

          end;

          then

          reconsider B as Subset-Family of M by TARSKI:def 3;



           A14: for P be 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

             A15: 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 in the topology of ( TOP-REAL n) by PRE_TOPC:def 2, A15, YELLOW_8: 12;

            then

             A16: X1 is open by PRE_TOPC:def 2;

            reconsider U1 = (M | U) as non empty TopStruct by A8, A7;

            reconsider g = (f " ) as Function of the TopStruct of ( TOP-REAL n), U1;



             A17: g is being_homeomorphism by A3, TOPS_2: 56;



             A18: (g .: X1) is open by A16, A17, TOPGRP_1: 25;

            (g .: X1) in the topology of (M | U) by A18, PRE_TOPC:def 2;

            then

            consider Q be Subset of M such that

             A19: Q in the topology of M & (g .: X1) = (Q /\ ( [#] (M | U))) by PRE_TOPC:def 4;

            ( [#] (M | U)) = U by PRE_TOPC:def 5;



            then

             A20: P = (Q /\ (U /\ ( Int U))) by A19, A15, XBOOLE_1: 16

            .= (Q /\ ( Int U)) by TOPS_1: 16, XBOOLE_1: 28;

            Q is open by A19, PRE_TOPC:def 2;

            hence P is open by A20;

          end;

          for Y be 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

             A21: Y = F(X1) & X1 in B1;

            reconsider g = f as Function;

             [p, (g . p)] in g by A8, A7, A5, FUNCT_1:def 2;

            then [q, p] in (g ~ ) by RELAT_1:def 7;

            then [q, p] in (g " ) by A4, FUNCT_1:def 5;

            then

             A22: [q, p] in (f " ) by A6, A4, TOPS_2:def 4;

            q in X1 by A21, YELLOW_8: 12;

            then p in ((f " ) .: X1) by A22, RELAT_1:def 13;

            hence p in Y by A21, A8, XBOOLE_0:def 4;

          end;

          then

           A23: p in ( Intersect B) by SETFAM_1: 43;

          for S be Subset of M st S is open & p in S holds ex V be Subset of M st V in B & V c= S

          proof

            let S be Subset of M;

            assume

             A24: S is open & p in S;

            set S1 = (S /\ ( [#] (M | U)));

            S in the topology of M by A24, PRE_TOPC:def 2;

            then

             A25: S1 in the topology of (M | U) by PRE_TOPC:def 4;

            reconsider U1 = (M | U) as non empty TopStruct by A8, A7;

            reconsider S1 as Subset of U1;

            S1 is open by A25, PRE_TOPC:def 2;

            then

             A26: (f .: S1) is open by A3, TOPGRP_1: 25;

            reconsider S2 = (f .: S1) as Subset of ( TOP-REAL n);



             K: (f .: S1) in the topology of the TopStruct of ( TOP-REAL n) by A26, PRE_TOPC:def 2;

            reconsider g1 = f as Function;



             A28: [p, q] in f by A8, A7, A5, FUNCT_1:def 2;

            p in S1 by A9, A24, XBOOLE_0:def 4;

            then

             A29: q in S2 by A28, RELAT_1:def 13;

            consider W be Subset of ( TOP-REAL n) such that

             A30: W in B1 & W c= S2 by A29, K, PRE_TOPC:def 2, YELLOW_8: 13;

            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 A30;



             A31: (g1 " ) = (f " ) by A6, A4, TOPS_2:def 4;



             A32: ((f " ) .: (f .: S1)) = S1 by A31, A4, FUNCT_1: 107;



             A33: (((f " ) .: W) /\ ( Int U)) c= ((f " ) .: W) by XBOOLE_1: 17;



             A34: S1 c= S by XBOOLE_1: 17;

            ((f " ) .: W) c= ((f " ) .: (f .: S1)) by A30, RELAT_1: 123;

            hence V c= S by A33, A32, A34;

          end;

          then

          reconsider B as Basis of p by A14, A23, TOPS_2:def 1, YELLOW_8:def 1;

          take B;

          thus B is countable by A12, CARD_3:def 14;

        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: 93;

    registration

      cluster 0 -locally_euclidean -> discrete for non empty TopSpace;

      coherence

      proof

        let M be non empty TopSpace;

        assume

         A1: M is 0 -locally_euclidean;

        for X be Subset of M, p be 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: 16;



           A5: p in U by A4, CONNSP_2:def 1;

          consider f be Function of (M | U), T such that

           A6: f is being_homeomorphism by T_0TOPSP:def 1, A3, METRIZTS:def 1;

          consider V be Subset of M such that

           A7: V is open & V c= U & p in V by CONNSP_2: 6;

          for x be object holds x in V iff x = p

          proof

            let x be object;

            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 5;

              then

               A10: x in ( dom f) by A6, TOPS_2:def 5;

              then

               A11: (f . x) in ( rng f) by FUNCT_1: 3;

              p in ( [#] (M | U)) by A5, PRE_TOPC:def 5;

              then

               A12: p in ( dom f) by A6, TOPS_2:def 5;

              then

               A13: (f . p) in ( rng f) by FUNCT_1: 3;

              (f . x) = ( 0. ( TOP-REAL 0 )) by Lm2, A11

              .= (f . p) by Lm2, A13;

              hence x = p by A9, A10, A12;

            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: 17;

      end;

      cluster discrete -> 0 -locally_euclidean for non empty TopSpace;

      coherence

      proof



         A14: ( [#] T) = {( 0. ( TOP-REAL 0 ))} by Lm2, EUCLID: 22, EUCLID: 77;

        let M be non empty TopSpace;

        assume

         A15: M is discrete;

        for p be Point of M holds ex U be 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: 31;



           A16: U is open & p in U by A15, TARSKI:def 1, TDLAT_3: 15;

          then

          reconsider U as a_neighborhood of p by CONNSP_2: 3;

          take U;

          set f = { [p, ( 0. ( TOP-REAL 0 ))]};



           A17: p in ( [#] (M | U)) by A16, PRE_TOPC:def 5;



           A19: ( dom f) = U by RELAT_1: 9;

          then

           A20: ( dom f) = ( [#] (M | U)) by PRE_TOPC:def 5;

          then

          reconsider f as Function of (M | U), T by A17, Lm2, ZFMISC_1: 87, FUNCT_2:def 1, ZFMISC_1: 31;



           A21: ( rng f) = ( [#] T) by A14, RELAT_1: 9;

          for P be 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;

              thus thesis by A22;

            end;

              suppose

               A23: P is non empty;

              then P = ( [#] (M | U)) by A20, A19, ZFMISC_1: 33;

              hence P is closed implies (f .: P) is closed by A21, A20, RELAT_1: 113;

              thus (f .: P) is closed implies P is closed by A23, A20, A19, ZFMISC_1: 33;

            end;

          end;

          then ((M | U),T) are_homeomorphic by T_0TOPSP:def 1, A20, A21, TOPS_2: 58;

          hence (U,( [#] ( TOP-REAL 0 ))) are_homeomorphic by METRIZTS:def 1;

        end;

        hence M is 0 -locally_euclidean by Th13;

      end;

    end

    definition

      let n, M;

      :: MFOLD_1:def4

      attr M is n -manifold means M is second-countable Hausdorffn -locally_euclidean;

    end

    registration

      let n;

      cluster without_boundaryn -manifold for non empty TopSpace;

      existence

      proof

        take ( TOP-REAL n);

        thus thesis;

      end;

    end

    registration

      cluster second-countable discrete -> 0 -locally_euclidean second-countable Hausdorff for non empty TopSpace;

      coherence ;

    end

    registration

      let n;

      cluster n -manifold -> second-countable Hausdorffn -locally_euclidean for non empty TopSpace;

      correctness ;

      cluster second-countable Hausdorffn -locally_euclidean -> n -manifold for non empty TopSpace;

      correctness ;

    end

    registration

      let n;

      let M be without_boundaryn -manifold non empty TopSpace;

      cluster open -> without_boundaryn -manifold for 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 4;

        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 5

        .= the carrier of (M | X1);

        then

         A3: the TopStruct of X = the TopStruct of (M | X1) by TSEP_1: 5;

        for p be Point of X holds ex U be a_neighborhood of p, S be 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;

          consider f be Function of (M | U2), (( TOP-REAL n) | S2) such that

           A11: f is being_homeomorphism by T_0TOPSP:def 1, A9, METRIZTS: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: 3;

          U c= U2 by XBOOLE_1: 17;

          then U c= ( [#] (M | U2)) by PRE_TOPC:def 5;

          then

          reconsider U3 = U as Subset of (M | U2);



           A13: (((M | U2) | U3),((( TOP-REAL n) | S2) | (f .: U3))) are_homeomorphic by METRIZTS:def 1, A11, METRIZTS: 3;

          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: 18;

          reconsider f2 = f as Function of M2, T2;



           A14: for P be 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 5;



           A16: X1 in the topology of M by PRE_TOPC:def 2;

          U2 = ( [#] M2) by PRE_TOPC:def 5;

          then U3 in the topology of M2 by A16, PRE_TOPC:def 4;

          then

          reconsider S = (f .: U3) as open Subset of T2 by A14, PRE_TOPC:def 2;

          S in the topology of T2 by PRE_TOPC:def 2;

          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 4;



           A18: ( [#] T2) = S2 by PRE_TOPC:def 5;

          S2 in the topology of ( TOP-REAL n) by PRE_TOPC:def 2;

          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 2;

          take U, S;

          U c= X1;

          then U c= ( [#] (M | X1)) by PRE_TOPC:def 5;

          then

          reconsider U4 = U as Subset of (M | X1);

          reconsider U5 = U as Subset of M;



           A19: ((M | X1) | U4) = (M | U5) by GOBOARD9: 2;

          ((M | U2) | U3) = (M | U5) by GOBOARD9: 2;

          then

           A20: the TopStruct of (X | U) = the TopStruct of ((M | U2) | U3) by A19, A3, PRE_TOPC: 36;

          ((( TOP-REAL n) | S2) | (f .: U3)) = (( TOP-REAL n) | S) by A15, PRE_TOPC: 7;

          hence (U,S) are_homeomorphic by A13, A20, METRIZTS:def 1;

        end;

        hence thesis by Def4;

      end;

    end