:: MFOLD_1 semantic presentation begin registration let x, y be set ; cluster{[x,y]} -> one-to-one ; correctness coherence {[x,y]} is one-to-one ; proof set f = {[x,y]}; let x1, x2 be set ; :: according to FUNCT_1:def_4 ::_thesis: ( not x1 in dom {[x,y]} or not x2 in dom {[x,y]} or not {[x,y]} . x1 = {[x,y]} . x2 or x1 = x2 ) assume ( x1 in dom {[x,y]} & x2 in dom {[x,y]} & {[x,y]} . x1 = {[x,y]} . x2 ) ; ::_thesis: x1 = 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 ; ::_thesis: verum end; end; theorem Th1: :: MFOLD_1:1 for T being non empty TopSpace holds T,T | ([#] T) are_homeomorphic proof let X be non empty TopSpace; ::_thesis: X,X | ([#] X) are_homeomorphic set f = id X; A1: dom (id X) = [#] X by RELAT_1:45; A2: [#] (X | ([#] X)) = the carrier of TopStruct(# the carrier of X, the topology of X #) by TSEP_1:93 .= [#] X ; then A3: rng (id X) = [#] (X | ([#] X)) by RELAT_1:45; reconsider f = id X 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; ::_thesis: ( P is closed implies (f ") " P is closed ) assume P is closed ; ::_thesis: (f ") " P is closed then ([#] X) \ P is open by PRE_TOPC:def_3; then A4: ([#] X) \ P in the topology of X by PRE_TOPC:def_2; A5: for x being set holds ( x in (f ") " P iff x in P ) proof let x be set ; ::_thesis: ( x in (f ") " P iff x in P ) hereby ::_thesis: ( x in P implies x in (f ") " P ) assume A6: x in (f ") " P ; ::_thesis: x in P x in f .: P by A6, A3, TOPS_2:54; then consider y being 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; ::_thesis: verum end; assume A8: x in P ; ::_thesis: x in (f ") " 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:54; ::_thesis: verum end; A9: ([#] X) \ P = ([#] (X | ([#] X))) \ ((f ") " P) by A2, A5, TARSKI:1; ([#] 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_4; then ([#] (X | ([#] X))) \ ((f ") " P) is open by A9, PRE_TOPC:def_2; hence (f ") " P is closed by PRE_TOPC:def_3; ::_thesis: verum end; then A10: f " is continuous by PRE_TOPC:def_6; f is continuous by JGRAPH_1:45; then f is being_homeomorphism by A1, A3, A10, TOPS_2:def_5; hence X,X | ([#] X) are_homeomorphic by T_0TOPSP:def_1; ::_thesis: verum end; theorem Th2: :: MFOLD_1:2 for n being Nat for X being non empty SubSpace of TOP-REAL n for f being Function of X,R^1 st f is continuous holds ex g being Function of X,(TOP-REAL n) st ( ( for a being Point of X for b being Point of (TOP-REAL n) for r being real number st a = b & f . a = r holds g . b = r * b ) & g is continuous ) proof let n be Nat; ::_thesis: for X being non empty SubSpace of TOP-REAL n for f being Function of X,R^1 st f is continuous holds ex g being Function of X,(TOP-REAL n) st ( ( for a being Point of X for b being Point of (TOP-REAL n) for r being real number st a = b & f . a = r holds g . b = r * b ) & g is continuous ) let X be non empty SubSpace of TOP-REAL n; ::_thesis: for f being Function of X,R^1 st f is continuous holds ex g being Function of X,(TOP-REAL n) st ( ( for a being Point of X for b being Point of (TOP-REAL n) for r being real number st a = b & f . a = r holds g . b = r * b ) & g is continuous ) let f be Function of X,R^1; ::_thesis: ( f is continuous implies ex g being Function of X,(TOP-REAL n) st ( ( for a being Point of X for b being Point of (TOP-REAL n) for r being real number st a = b & f . a = r holds g . b = r * b ) & g is continuous ) ) assume A1: f is continuous ; ::_thesis: ex g being Function of X,(TOP-REAL n) st ( ( for a being Point of X for b being Point of (TOP-REAL n) for r being real number st a = b & f . a = r holds g . b = r * b ) & g is continuous ) defpred S1[ set , set ] means for b being Point of (TOP-REAL n) for 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 S1[x,y] proof let x be Element of X; ::_thesis: ex y being Point of (TOP-REAL n) st S1[x,y] reconsider r = f . x as Real by TOPMETR:17; A3: x in the carrier of X ; [#] X c= [#] (TOP-REAL n) by PRE_TOPC:def_4; then reconsider p = x as Point of (TOP-REAL n) by A3; set y = r * p; take r * p ; ::_thesis: S1[x,r * p] thus S1[x,r * p] ; ::_thesis: verum end; ex g being Function of the carrier of X, the carrier of (TOP-REAL n) st for x being Element of X holds S1[x,g . x] from FUNCT_2:sch_3(A2); then consider g being Function of X,(TOP-REAL n) such that A4: for x being Element of X for b being Point of (TOP-REAL n) for r being real number st x = b & f . x = r holds g . x = r * b ; take g ; ::_thesis: ( ( for a being Point of X for b being Point of (TOP-REAL n) for r being real number st a = b & f . a = r holds g . b = r * b ) & g is continuous ) for p being Point of X for 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; ::_thesis: for 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 ) let V be Subset of (TOP-REAL n); ::_thesis: ( g . p in V & V is open implies ex W being Subset of X st ( p in W & W is open & g .: W c= V ) ) reconsider n1 = n as Element of NAT by ORDINAL1:def_12; reconsider gp = g . p as Point of (Euclid n) by TOPREAL3:8; A5: p in the carrier of X ; [#] X c= [#] (TOP-REAL n) by PRE_TOPC:def_4; then reconsider pp = p as Point of (TOP-REAL n1) by A5; reconsider fp = f . p as real number ; assume ( g . p in V & V is open ) ; ::_thesis: ex W being Subset of X st ( p in W & W is open & g .: W c= V ) then g . p in Int V by TOPS_1:23; then consider r0 being real number such that A6: r0 > 0 and A7: Ball (gp,r0) c= V by GOBOARD6:5; percases ( fp = 0 or fp <> 0 ) ; supposeA8: fp = 0 ; ::_thesis: ex W being Subset of X st ( p in W & W is open & g .: W c= V ) 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 A9: W2 is open by PRE_TOPC:def_2; p in Ball (pp,(r0 / 2)) by A6, JORDAN:16; then A10: p in W2 by XBOOLE_0:def_4; set WW2 = { |.p2.| where p2 is Point of (TOP-REAL n) : p2 in W2 } ; A11: |.pp.| in { |.p2.| where p2 is Point of (TOP-REAL n) : p2 in W2 } by A10; for x being set st x in { |.p2.| where p2 is Point of (TOP-REAL n) : p2 in W2 } holds x is real proof let x be set ; ::_thesis: ( x in { |.p2.| where p2 is Point of (TOP-REAL n) : p2 in W2 } implies x is real ) assume x in { |.p2.| where p2 is Point of (TOP-REAL n) : p2 in W2 } ; ::_thesis: x is real then consider p2 being Point of (TOP-REAL n1) such that A12: ( x = |.p2.| & p2 in W2 ) ; thus x is real by A12; ::_thesis: verum end; then reconsider WW2 = { |.p2.| where p2 is Point of (TOP-REAL n) : p2 in W2 } as non empty real-membered set by A11, 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 ; ::_thesis: ( x in WW2 implies x <= |.pp.| + (r0 / 2) ) assume x in WW2 ; ::_thesis: x <= |.pp.| + (r0 / 2) then consider p2 being Point of (TOP-REAL n1) such that A13: ( x = |.p2.| & p2 in W2 ) ; p2 in Ball (pp,(r0 / 2)) by A13, XBOOLE_0:def_4; then A14: |.(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 A14, XXREAL_0:2; then (|.p2.| - |.pp.|) + |.pp.| <= (r0 / 2) + |.pp.| by XREAL_1:6; hence x <= |.pp.| + (r0 / 2) by A13; ::_thesis: verum 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 ; A15: m >= 0 proof assume A16: m < 0 ; ::_thesis: contradiction A17: m is UpperBound of WW2 by XXREAL_2:def_3; |.pp.| in WW2 by A10; hence contradiction by A16, A17, XXREAL_2:def_1; ::_thesis: verum end; percases ( m = 0 or m > 0 ) by A15; supposeA18: m = 0 ; ::_thesis: ex W being Subset of X st ( p in W & W is open & g .: W c= V ) set G1 = REAL ; REAL in the topology of R^1 by PRE_TOPC:def_1, TOPMETR:17; then reconsider G1 = REAL as open Subset of R^1 by PRE_TOPC:def_2; fp in G1 by XREAL_0:def_1; then consider W1 being Subset of X such that A19: p in W1 and A20: W1 is open and f .: W1 c= G1 by A1, JGRAPH_2:10; reconsider W3 = W1 /\ W2 as Subset of X ; take W3 ; ::_thesis: ( p in W3 & W3 is open & g .: W3 c= V ) thus p in W3 by A19, A10, XBOOLE_0:def_4; ::_thesis: ( W3 is open & g .: W3 c= V ) thus W3 is open by A20, A9; ::_thesis: g .: W3 c= V g .: W3 c= Ball (gp,r0) proof let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in g .: W3 or x in Ball (gp,r0) ) assume x in g .: W3 ; ::_thesis: x in Ball (gp,r0) then consider q being set such that A21: q in dom g and A22: q in W3 and A23: g . q = x by FUNCT_1:def_6; reconsider q = q as Point of X by A21; A24: 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) by A24; reconsider fq = f . q as real number ; A25: x = fq * qq by A4, A23; 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 A25; A26: gpp = fp * pp by A4; reconsider r2 = fq - fp as Real by XREAL_0:def_1; A27: (abs (fq - fp)) * |.qq.| = (abs r2) * |.qq.| .= |.((fq - fp) * qq).| by TOPRNS_1:7 ; qq in W2 by A22, XBOOLE_0:def_4; then |.qq.| in WW2 ; then A28: |.qq.| <= m by XXREAL_2:4; A29: gpp = 0. (TOP-REAL n1) by A26, A8, EUCLID:29; |.(gqq + (- gpp)).| <= |.gqq.| + |.(- gpp).| by EUCLID_2:52; then |.(gqq + (- gpp)).| <= |.gqq.| + |.(0. (TOP-REAL n1)).| by A29, JGRAPH_5:10; then |.(gqq + (- gpp)).| <= |.gqq.| + 0 by EUCLID_2:39; then |.(gqq - gpp).| < r0 by A4, A23, A8, A28, A27, A6, A18; then gqq in Ball (gpp,r0) ; hence x in Ball (gp,r0) by TOPREAL9:13; ::_thesis: verum end; hence g .: W3 c= V by A7, XBOOLE_1:1; ::_thesis: verum end; supposeA30: m > 0 ; ::_thesis: ex W being Subset of X st ( p in W & W is open & g .: W c= V ) set G1 = ].(fp - (r0 / m)),(fp + (r0 / m)).[; reconsider G1 = ].(fp - (r0 / m)),(fp + (r0 / m)).[ as open Subset of R^1 by JORDAN6:35, TOPMETR:17, XXREAL_1:225; A31: 0 + fp < (r0 / m) + fp by A30, A6, XREAL_1:6; (- (r0 / m)) + fp < 0 + fp by A30, A6, XREAL_1:6; then fp in G1 by A31, XXREAL_1:4; then consider W1 being Subset of X such that A32: p in W1 and A33: W1 is open and A34: f .: W1 c= G1 by A1, JGRAPH_2:10; reconsider W3 = W1 /\ W2 as Subset of X ; take W3 ; ::_thesis: ( p in W3 & W3 is open & g .: W3 c= V ) thus p in W3 by A32, A10, XBOOLE_0:def_4; ::_thesis: ( W3 is open & g .: W3 c= V ) thus W3 is open by A33, A9; ::_thesis: g .: W3 c= V g .: W3 c= Ball (gp,r0) proof let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in g .: W3 or x in Ball (gp,r0) ) assume x in g .: W3 ; ::_thesis: x in Ball (gp,r0) then consider q being set such that A35: q in dom g and A36: q in W3 and A37: g . q = x by FUNCT_1:def_6; reconsider q = q as Point of X by A35; A38: 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) by A38; reconsider fq = f . q as real number ; A39: x = fq * qq by A4, A37; 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 A39; A40: gpp = fp * pp by A4; reconsider r2 = fq as Real by XREAL_0:def_1; A41: (abs fq) * |.qq.| = (abs r2) * |.qq.| .= |.(fq * qq).| by TOPRNS_1:7 ; A42: q in dom f by A38, FUNCT_2:def_1; q in W1 by A36, XBOOLE_0:def_4; then f . q in f .: W1 by A42, FUNCT_1:def_6; then abs (fq - fp) < r0 / m by A34, RCOMP_1:1; then (abs fq) * m < (r0 / m) * m by A8, A30, XREAL_1:68; then (abs fq) * m < r0 / (m / m) by XCMPLX_1:82; then A43: (abs fq) * m < r0 / 1 by A30, XCMPLX_1:60; qq in W2 by A36, XBOOLE_0:def_4; then |.qq.| in WW2 ; then |.qq.| <= m by XXREAL_2:4; then A44: |.qq.| * (abs fq) <= m * (abs fq) by XREAL_1:64; A45: gpp = 0. (TOP-REAL n1) by A40, A8, EUCLID:29; A46: |.gqq.| < r0 by A39, A44, A41, A43, XXREAL_0:2; |.(gqq + (- gpp)).| <= |.gqq.| + |.(- gpp).| by EUCLID_2:52; then |.(gqq + (- gpp)).| <= |.gqq.| + |.(0. (TOP-REAL n1)).| by A45, JGRAPH_5:10; then |.(gqq + (- gpp)).| <= |.gqq.| + 0 by EUCLID_2:39; then |.(gqq - gpp).| < r0 by A46, XXREAL_0:2; then gqq in Ball (gpp,r0) ; hence x in Ball (gp,r0) by TOPREAL9:13; ::_thesis: verum end; hence g .: W3 c= V by A7, XBOOLE_1:1; ::_thesis: verum end; end; end; supposeA47: fp <> 0 ; ::_thesis: ex W being Subset of X st ( p in W & W is open & g .: W c= V ) 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_2; then W2 in the topology of X by PRE_TOPC:def_4; then A48: W2 is open by PRE_TOPC:def_2; p in Ball (pp,((r0 / 2) / (abs fp))) by A47, A6, JORDAN:16; then A49: p in W2 by XBOOLE_0:def_4; set WW2 = { |.p2.| where p2 is Point of (TOP-REAL n) : p2 in W2 } ; A50: |.pp.| in { |.p2.| where p2 is Point of (TOP-REAL n) : p2 in W2 } by A49; for x being set st x in { |.p2.| where p2 is Point of (TOP-REAL n) : p2 in W2 } holds x is real proof let x be set ; ::_thesis: ( x in { |.p2.| where p2 is Point of (TOP-REAL n) : p2 in W2 } implies x is real ) assume x in { |.p2.| where p2 is Point of (TOP-REAL n) : p2 in W2 } ; ::_thesis: x is real then consider p2 being Point of (TOP-REAL n1) such that A51: ( x = |.p2.| & p2 in W2 ) ; thus x is real by A51; ::_thesis: verum end; then reconsider WW2 = { |.p2.| where p2 is Point of (TOP-REAL n) : p2 in W2 } as non empty real-membered set by A50, 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 ; ::_thesis: ( x in WW2 implies x <= |.pp.| + ((r0 / 2) / (abs fp)) ) assume x in WW2 ; ::_thesis: x <= |.pp.| + ((r0 / 2) / (abs fp)) then consider p2 being Point of (TOP-REAL n1) such that A52: ( x = |.p2.| & p2 in W2 ) ; p2 in Ball (pp,((r0 / 2) / (abs fp))) by A52, XBOOLE_0:def_4; then A53: |.(p2 - pp).| < (r0 / 2) / (abs 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) / (abs fp) by A53, XXREAL_0:2; then (|.p2.| - |.pp.|) + |.pp.| <= ((r0 / 2) / (abs fp)) + |.pp.| by XREAL_1:6; hence x <= |.pp.| + ((r0 / 2) / (abs fp)) by A52; ::_thesis: verum 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 ; A54: m >= 0 proof assume A55: m < 0 ; ::_thesis: contradiction A56: m is UpperBound of WW2 by XXREAL_2:def_3; |.pp.| in WW2 by A49; hence contradiction by A55, A56, XXREAL_2:def_1; ::_thesis: verum end; percases ( m = 0 or m > 0 ) by A54; supposeA57: m = 0 ; ::_thesis: ex W being Subset of X st ( p in W & W is open & g .: W c= V ) set G1 = REAL ; REAL in the topology of R^1 by PRE_TOPC:def_1, TOPMETR:17; then reconsider G1 = REAL as open Subset of R^1 by PRE_TOPC:def_2; fp in G1 by XREAL_0:def_1; then consider W1 being Subset of X such that A58: p in W1 and A59: W1 is open and f .: W1 c= G1 by A1, JGRAPH_2:10; reconsider W3 = W1 /\ W2 as Subset of X ; take W3 ; ::_thesis: ( p in W3 & W3 is open & g .: W3 c= V ) thus p in W3 by A58, A49, XBOOLE_0:def_4; ::_thesis: ( W3 is open & g .: W3 c= V ) thus W3 is open by A59, A48; ::_thesis: g .: W3 c= V g .: W3 c= Ball (gp,r0) proof let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in g .: W3 or x in Ball (gp,r0) ) assume x in g .: W3 ; ::_thesis: x in Ball (gp,r0) then consider q being set such that A60: q in dom g and A61: q in W3 and A62: g . q = x by FUNCT_1:def_6; reconsider q = q as Point of X by A60; A63: 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) by A63; reconsider fq = f . q as real number ; A64: x = fq * qq by A4, A62; 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 A64; A65: 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; A66: (abs (fq - fp)) * |.qq.| = (abs r2) * |.qq.| .= |.((fq - fp) * qq).| by TOPRNS_1:7 ; qq in W2 by A61, XBOOLE_0:def_4; then |.qq.| in WW2 ; then A67: |.qq.| <= m by XXREAL_2:4; A68: (abs fp) * |.(qq - pp).| = (abs r3) * |.(qq - pp).| .= |.(fp * (qq - pp)).| by TOPRNS_1:7 ; qq in W2 by A61, 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 A47, XREAL_1:68; then (abs fp) * |.(qq - pp).| < (r0 / 2) / ((abs fp) / (abs fp)) by XCMPLX_1:81; then A69: (abs fp) * |.(qq - pp).| < (r0 / 2) / 1 by A47, XCMPLX_1:60; A70: |.((fq - fp) * qq).| + |.(fp * (qq - pp)).| < (r0 / 2) + (r0 / 2) by A67, A69, A68, A66, A57, XREAL_1:8; |.(((fq - fp) * qq) + (fp * (qq - pp))).| <= |.((fq - fp) * qq).| + |.(fp * (qq - pp)).| by EUCLID_2:52; then A71: |.(((fq - fp) * qq) + (fp * (qq - pp))).| < r0 by A70, XXREAL_0:2; ((fq - fp) * qq) + (fp * (qq - pp)) = ((fq * qq) - (fp * qq)) + (fp * (qq - pp)) by EUCLID:50 .= ((fq * qq) - (fp * qq)) + ((fp * qq) - (fp * pp)) by EUCLID:49 .= (((fq * qq) - (fp * qq)) + (fp * qq)) - (fp * pp) by EUCLID:45 .= (fq * qq) - (fp * pp) by EUCLID:48 ; then gqq in Ball (gpp,r0) by A64, A71, A65; hence x in Ball (gp,r0) by TOPREAL9:13; ::_thesis: verum end; hence g .: W3 c= V by A7, XBOOLE_1:1; ::_thesis: verum end; supposeA72: m > 0 ; ::_thesis: ex W being Subset of X st ( p in W & W is open & g .: W c= V ) set G1 = ].(fp - ((r0 / 2) / m)),(fp + ((r0 / 2) / m)).[; reconsider G1 = ].(fp - ((r0 / 2) / m)),(fp + ((r0 / 2) / m)).[ as open Subset of R^1 by JORDAN6:35, TOPMETR:17, XXREAL_1:225; A73: 0 + fp < ((r0 / 2) / m) + fp by A72, A6, XREAL_1:6; (- ((r0 / 2) / m)) + fp < 0 + fp by A72, A6, XREAL_1:6; then fp in G1 by A73, XXREAL_1:4; then consider W1 being Subset of X such that A74: p in W1 and A75: W1 is open and A76: f .: W1 c= G1 by A1, JGRAPH_2:10; reconsider W3 = W1 /\ W2 as Subset of X ; take W3 ; ::_thesis: ( p in W3 & W3 is open & g .: W3 c= V ) thus p in W3 by A74, A49, XBOOLE_0:def_4; ::_thesis: ( W3 is open & g .: W3 c= V ) thus W3 is open by A75, A48; ::_thesis: g .: W3 c= V g .: W3 c= Ball (gp,r0) proof let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in g .: W3 or x in Ball (gp,r0) ) assume x in g .: W3 ; ::_thesis: x in Ball (gp,r0) then consider q being set such that A77: q in dom g and A78: q in W3 and A79: g . q = x by FUNCT_1:def_6; reconsider q = q as Point of X by A77; A80: 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) by A80; reconsider fq = f . q as real number ; A81: x = fq * qq by A4, A79; 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 A81; A82: 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; A83: (abs (fq - fp)) * |.qq.| = (abs r2) * |.qq.| .= |.((fq - fp) * qq).| by TOPRNS_1:7 ; A84: q in dom f by A80, FUNCT_2:def_1; q in W1 by A78, XBOOLE_0:def_4; then f . q in f .: W1 by A84, FUNCT_1:def_6; then abs (fq - fp) < (r0 / 2) / m by A76, RCOMP_1:1; then (abs (fq - fp)) * m < ((r0 / 2) / m) * m by A72, XREAL_1:68; then (abs (fq - fp)) * m < (r0 / 2) / (m / m) by XCMPLX_1:82; then A85: (abs (fq - fp)) * m < (r0 / 2) / 1 by A72, XCMPLX_1:60; qq in W2 by A78, 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:64; then A86: |.((fq - fp) * qq).| < r0 / 2 by A83, A85, XXREAL_0:2; A87: (abs fp) * |.(qq - pp).| = (abs r3) * |.(qq - pp).| .= |.(fp * (qq - pp)).| by TOPRNS_1:7 ; qq in W2 by A78, 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 A47, XREAL_1:68; then (abs fp) * |.(qq - pp).| < (r0 / 2) / ((abs fp) / (abs fp)) by XCMPLX_1:81; then A88: (abs fp) * |.(qq - pp).| < (r0 / 2) / 1 by A47, XCMPLX_1:60; A89: |.((fq - fp) * qq).| + |.(fp * (qq - pp)).| < (r0 / 2) + (r0 / 2) by A86, A88, A87, XREAL_1:8; |.(((fq - fp) * qq) + (fp * (qq - pp))).| <= |.((fq - fp) * qq).| + |.(fp * (qq - pp)).| by EUCLID_2:52; then A90: |.(((fq - fp) * qq) + (fp * (qq - pp))).| < r0 by A89, XXREAL_0:2; ((fq - fp) * qq) + (fp * (qq - pp)) = ((fq * qq) - (fp * qq)) + (fp * (qq - pp)) by EUCLID:50 .= ((fq * qq) - (fp * qq)) + ((fp * qq) - (fp * pp)) by EUCLID:49 .= (((fq * qq) - (fp * qq)) + (fp * qq)) - (fp * pp) by EUCLID:45 .= (fq * qq) - (fp * pp) by EUCLID:48 ; then gqq in Ball (gpp,r0) by A81, A82, A90; hence x in Ball (gp,r0) by TOPREAL9:13; ::_thesis: verum end; hence g .: W3 c= V by A7, XBOOLE_1:1; ::_thesis: verum end; end; end; end; end; hence ( ( for a being Point of X for b being Point of (TOP-REAL n) for r being real number st a = b & f . a = r holds g . b = r * b ) & g is continuous ) by A4, JGRAPH_2:10; ::_thesis: verum end; definition let n be Nat; let S be Subset of (TOP-REAL n); attrS is ball means :Def1: :: MFOLD_1:def 1 ex p being Point of (TOP-REAL n) ex r being real number st S = Ball (p,r); end; :: deftheorem Def1 defines ball MFOLD_1:def_1_:_ for n being Nat for S being Subset of (TOP-REAL n) holds ( S is ball iff ex p being Point of (TOP-REAL n) ex r being real number st S = Ball (p,r) ); registration let n be Nat; cluster functional ball for Element of bool the carrier of (TOP-REAL n); correctness existence ex b1 being Subset of (TOP-REAL n) st b1 is ball ; proof take Ball ( the Point of (TOP-REAL n), the real number ) ; ::_thesis: Ball ( the Point of (TOP-REAL n), the real number ) is ball thus Ball ( the Point of (TOP-REAL n), the real number ) is ball by Def1; ::_thesis: verum end; cluster ball -> open for Element of bool the carrier of (TOP-REAL n); correctness coherence for b1 being Subset of (TOP-REAL n) st b1 is ball holds b1 is open ; proof let S be Subset of (TOP-REAL n); ::_thesis: ( S is ball implies S is open ) assume S is ball ; ::_thesis: S is open then ex p being Point of (TOP-REAL n) ex r being real number st S = Ball (p,r) by Def1; hence S is open ; ::_thesis: verum end; end; registration let n be Nat; cluster non empty functional ball for Element of bool the carrier of (TOP-REAL n); correctness existence ex b1 being Subset of (TOP-REAL n) st ( not b1 is empty & b1 is ball ); proof reconsider S = Ball ((0. (TOP-REAL n)),1) as ball Subset of (TOP-REAL n) by Def1; take S ; ::_thesis: ( not S is empty & S is ball ) thus ( not S is empty & S is ball ) ; ::_thesis: verum end; end; theorem Th3: :: MFOLD_1:3 for n being Nat for p being Point of (TOP-REAL n) 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 n be Nat; ::_thesis: for p being Point of (TOP-REAL n) 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 ) let p be Point of (TOP-REAL n); ::_thesis: 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 ) let S be open Subset of (TOP-REAL n); ::_thesis: ( p in S implies ex B being ball Subset of (TOP-REAL n) st ( B c= S & p in B ) ) assume A1: p in S ; ::_thesis: ex B being ball Subset of (TOP-REAL n) st ( B c= S & p in B ) 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 being Real such that A4: ( r > 0 & Ball (x,r) c= S ) by A1, A3, PCOMPS_1:def_4; reconsider r = r as real positive number 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 ; ::_thesis: ( B c= S & p in B ) reconsider p1 = p as Point of (TOP-REAL n1) ; Ball (x,r) = Ball (p1,r) by TOPREAL9:13; hence ( B c= S & p in B ) by A4, GOBOARD6:1; ::_thesis: verum end; definition let n be Nat; let p be Point of (TOP-REAL n); let r be real number ; func Tball (p,r) -> SubSpace of TOP-REAL n equals :: MFOLD_1:def 2 (TOP-REAL n) | (Ball (p,r)); correctness coherence (TOP-REAL n) | (Ball (p,r)) is SubSpace of TOP-REAL n; ; end; :: deftheorem defines Tball MFOLD_1:def_2_:_ for n being Nat for p being Point of (TOP-REAL n) for r being real number holds Tball (p,r) = (TOP-REAL n) | (Ball (p,r)); definition let n be Nat; func Tunit_ball n -> SubSpace of TOP-REAL n equals :: MFOLD_1:def 3 Tball ((0. (TOP-REAL n)),1); correctness coherence Tball ((0. (TOP-REAL n)),1) is SubSpace of TOP-REAL n; ; end; :: deftheorem defines Tunit_ball MFOLD_1:def_3_:_ for n being Nat holds Tunit_ball n = Tball ((0. (TOP-REAL n)),1); registration let n be Nat; cluster Tunit_ball n -> non empty ; correctness coherence not Tunit_ball n is empty ; ; let p be Point of (TOP-REAL n); let s be real positive number ; cluster Tball (p,s) -> non empty ; correctness coherence not Tball (p,s) is empty ; ; end; theorem Th4: :: MFOLD_1:4 for n being Nat for p being Point of (TOP-REAL n) for r being real number holds the carrier of (Tball (p,r)) = Ball (p,r) proof let n be Nat; ::_thesis: for p being Point of (TOP-REAL n) for r being real number holds the carrier of (Tball (p,r)) = Ball (p,r) let p be Point of (TOP-REAL n); ::_thesis: for r being real number holds the carrier of (Tball (p,r)) = Ball (p,r) let r be real number ; ::_thesis: the carrier of (Tball (p,r)) = Ball (p,r) [#] (Tball (p,r)) = Ball (p,r) by PRE_TOPC:def_5; hence the carrier of (Tball (p,r)) = Ball (p,r) ; ::_thesis: verum end; theorem Th5: :: MFOLD_1:5 for n being Nat for p being Point of (TOP-REAL n) st n <> 0 & p is Point of (Tunit_ball n) holds |.p.| < 1 proof let n be Nat; ::_thesis: for p being Point of (TOP-REAL n) st n <> 0 & p is Point of (Tunit_ball n) holds |.p.| < 1 let p be Point of (TOP-REAL n); ::_thesis: ( n <> 0 & p is Point of (Tunit_ball n) implies |.p.| < 1 ) reconsider j = 1 as real number ; assume n <> 0 ; ::_thesis: ( not p is Point of (Tunit_ball n) or |.p.| < 1 ) then reconsider n1 = n as non empty Element of NAT by ORDINAL1:def_12; assume p is Point of (Tunit_ball n) ; ::_thesis: |.p.| < 1 then p in the carrier of (Tball ((0. (TOP-REAL n1)),j)) ; then p in Ball ((0. (TOP-REAL n1)),1) by Th4; hence |.p.| < 1 by TOPREAL9:10; ::_thesis: verum end; theorem Th6: :: MFOLD_1:6 for n being Nat for f being Function of (Tunit_ball n),(TOP-REAL n) st n <> 0 & ( for a being Point of (Tunit_ball n) for 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 n be Nat; ::_thesis: for f being Function of (Tunit_ball n),(TOP-REAL n) st n <> 0 & ( for a being Point of (Tunit_ball n) for b being Point of (TOP-REAL n) st a = b holds f . a = (1 / (1 - (|.b.| * |.b.|))) * b ) holds f is being_homeomorphism let f be Function of (Tunit_ball n),(TOP-REAL n); ::_thesis: ( n <> 0 & ( for a being Point of (Tunit_ball n) for b being Point of (TOP-REAL n) st a = b holds f . a = (1 / (1 - (|.b.| * |.b.|))) * b ) implies f is being_homeomorphism ) assume that A1: n <> 0 and A2: for a being Point of (Tunit_ball n) for b being Point of (TOP-REAL n) st a = b holds f . a = (1 / (1 - (|.b.| * |.b.|))) * b ; ::_thesis: f is being_homeomorphism 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 empty Element of NAT by A1, ORDINAL1:def_12; 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 ; ::_thesis: ( y in [#] (TOP-REAL n1) implies ex x being set st [x,y] in f ) assume y in [#] (TOP-REAL n1) ; ::_thesis: ex x being set st [x,y] in f then reconsider py = y as Point of (TOP-REAL n1) ; percases ( |.py.| = 0 or |.py.| <> 0 ) ; supposeA5: |.py.| = 0 ; ::_thesis: ex x being set st [x,y] in f set x = py; |.(py - (0. (TOP-REAL n1))).| < 1 by A5, RLVECT_1:13; then py in Ball ((0. (TOP-REAL n)),1) ; then A6: py in dom f by A3, Th4; take py ; ::_thesis: [py,y] in f f . py = (1 / (1 - (|.py.| * |.py.|))) * py by A6, A2 .= py by A5, EUCLID:29 ; hence [py,y] in f by A6, FUNCT_1:def_2; ::_thesis: verum end; supposeA7: |.py.| <> 0 ; ::_thesis: ex x being set st [x,y] in f set p2 = |.py.| * |.py.|; set x = (2 / (1 + (sqrt (1 + (4 * (|.py.| * |.py.|)))))) * py; reconsider r = 2 / (1 + (sqrt (1 + (4 * (|.py.| * |.py.|))))) as Real ; A8: sqrt (1 + (4 * (|.py.| * |.py.|))) >= 0 by SQUARE_1:def_2; A9: |.((2 / (1 + (sqrt (1 + (4 * (|.py.| * |.py.|)))))) * py).| = (abs r) * |.py.| by TOPRNS_1:7 .= r * |.py.| by A8, ABSVALUE:def_1 ; |.((2 / (1 + (sqrt (1 + (4 * (|.py.| * |.py.|)))))) * py).| < 1 proof (|.py.| * 4) + (1 + (4 * (|.py.| * |.py.|))) > 0 + (1 + (4 * (|.py.| * |.py.|))) by A7, XREAL_1:6; then sqrt ((1 + (2 * |.py.|)) ^2) > sqrt (1 + (4 * (|.py.| * |.py.|))) by SQUARE_1:27; then 1 + (2 * |.py.|) > sqrt (1 + (4 * (|.py.| * |.py.|))) by SQUARE_1:22; then (1 + (2 * |.py.|)) - (sqrt (1 + (4 * (|.py.| * |.py.|)))) > (sqrt (1 + (4 * (|.py.| * |.py.|)))) - (sqrt (1 + (4 * (|.py.| * |.py.|)))) by XREAL_1:9; then ((1 - (sqrt (1 + (4 * (|.py.| * |.py.|))))) + (2 * |.py.|)) - (2 * |.py.|) > 0 - (2 * |.py.|) by XREAL_1:9; then (1 - (sqrt (1 + (4 * (|.py.| * |.py.|))))) * 1 > - (2 * |.py.|) ; then (1 - (sqrt (1 + (4 * (|.py.| * |.py.|))))) * ((1 + (sqrt (1 + (4 * (|.py.| * |.py.|))))) / (1 + (sqrt (1 + (4 * (|.py.| * |.py.|)))))) > - (2 * |.py.|) by A8, XCMPLX_1:60; then (1 - ((sqrt (1 + (4 * (|.py.| * |.py.|)))) ^2)) / (1 + (sqrt (1 + (4 * (|.py.| * |.py.|))))) > - (2 * |.py.|) ; then (1 - (1 + (4 * (|.py.| * |.py.|)))) / (1 + (sqrt (1 + (4 * (|.py.| * |.py.|))))) > - (2 * |.py.|) by SQUARE_1:def_2; then - ((4 * (|.py.| * |.py.|)) / (1 + (sqrt (1 + (4 * (|.py.| * |.py.|)))))) > - (2 * |.py.|) ; then ((2 * |.py.|) * (2 * |.py.|)) / (1 + (sqrt (1 + (4 * (|.py.| * |.py.|))))) < 2 * |.py.| by XREAL_1:24; then ((2 * |.py.|) * ((2 * |.py.|) / (1 + (sqrt (1 + (4 * (|.py.| * |.py.|))))))) / (2 * |.py.|) < (2 * |.py.|) / (2 * |.py.|) by A7, XREAL_1:74; then ((2 * |.py.|) * ((2 * |.py.|) / (1 + (sqrt (1 + (4 * (|.py.| * |.py.|))))))) / (2 * |.py.|) < 1 by A7, XCMPLX_1:60; then ((2 * |.py.|) / (1 + (sqrt (1 + (4 * (|.py.| * |.py.|)))))) / ((2 * |.py.|) / (2 * |.py.|)) < 1 by XCMPLX_1:77; then ((2 * |.py.|) / (1 + (sqrt (1 + (4 * (|.py.| * |.py.|)))))) / 1 < 1 by A7, XCMPLX_1:60; hence |.((2 / (1 + (sqrt (1 + (4 * (|.py.| * |.py.|)))))) * py).| < 1 by A9; ::_thesis: verum end; then |.(((2 / (1 + (sqrt (1 + (4 * (|.py.| * |.py.|)))))) * py) - (0. (TOP-REAL n1))).| < 1 by RLVECT_1:13; then (2 / (1 + (sqrt (1 + (4 * (|.py.| * |.py.|)))))) * py in Ball ((0. (TOP-REAL n1)),1) ; then A10: (2 / (1 + (sqrt (1 + (4 * (|.py.| * |.py.|)))))) * py in dom f by A3, Th4; take (2 / (1 + (sqrt (1 + (4 * (|.py.| * |.py.|)))))) * py ; ::_thesis: [((2 / (1 + (sqrt (1 + (4 * (|.py.| * |.py.|)))))) * py),y] in f A11: sqrt (1 + (4 * (|.py.| * |.py.|))) >= 0 by SQUARE_1:def_2; A12: 1 - (sqrt (1 + (4 * (|.py.| * |.py.|)))) <> 0 proof assume 1 - (sqrt (1 + (4 * (|.py.| * |.py.|)))) = 0 ; ::_thesis: contradiction then (sqrt (1 + (4 * (|.py.| * |.py.|)))) ^2 = 1 ; then 1 + (4 * (|.py.| * |.py.|)) = 1 by SQUARE_1:def_2; hence contradiction by A7; ::_thesis: verum end; |.((2 / (1 + (sqrt (1 + (4 * (|.py.| * |.py.|)))))) * py).| * |.((2 / (1 + (sqrt (1 + (4 * (|.py.| * |.py.|)))))) * py).| = ((2 / (1 + (sqrt (1 + (4 * (|.py.| * |.py.|)))))) * (2 / (1 + (sqrt (1 + (4 * (|.py.| * |.py.|))))))) * (|.py.| * |.py.|) by A9 .= ((2 * 2) / ((1 + (sqrt (1 + (4 * (|.py.| * |.py.|))))) * (1 + (sqrt (1 + (4 * (|.py.| * |.py.|))))))) * (|.py.| * |.py.|) by XCMPLX_1:76 .= (4 / ((1 + (2 * (sqrt (1 + (4 * (|.py.| * |.py.|)))))) + ((sqrt (1 + (4 * (|.py.| * |.py.|)))) ^2))) * (|.py.| * |.py.|) .= (4 / ((1 + (2 * (sqrt (1 + (4 * (|.py.| * |.py.|)))))) + (1 + (4 * (|.py.| * |.py.|))))) * (|.py.| * |.py.|) by SQUARE_1:def_2 .= (4 / (2 * ((1 + (sqrt (1 + (4 * (|.py.| * |.py.|))))) + (2 * (|.py.| * |.py.|))))) * (|.py.| * |.py.|) .= ((4 / 2) / ((1 + (sqrt (1 + (4 * (|.py.| * |.py.|))))) + (2 * (|.py.| * |.py.|)))) * (|.py.| * |.py.|) by XCMPLX_1:78 .= (2 * (|.py.| * |.py.|)) / ((1 + (2 * (|.py.| * |.py.|))) + (sqrt (1 + (4 * (|.py.| * |.py.|))))) ; then A13: 1 - (|.((2 / (1 + (sqrt (1 + (4 * (|.py.| * |.py.|)))))) * py).| * |.((2 / (1 + (sqrt (1 + (4 * (|.py.| * |.py.|)))))) * py).|) = (((1 + (2 * (|.py.| * |.py.|))) + (sqrt (1 + (4 * (|.py.| * |.py.|))))) / ((1 + (2 * (|.py.| * |.py.|))) + (sqrt (1 + (4 * (|.py.| * |.py.|)))))) + (- ((2 * (|.py.| * |.py.|)) / ((1 + (2 * (|.py.| * |.py.|))) + (sqrt (1 + (4 * (|.py.| * |.py.|))))))) by A11, XCMPLX_1:60 .= ((1 + (sqrt (1 + (4 * (|.py.| * |.py.|))))) / ((1 + (2 * (|.py.| * |.py.|))) + (sqrt (1 + (4 * (|.py.| * |.py.|)))))) * 1 .= ((1 + (sqrt (1 + (4 * (|.py.| * |.py.|))))) / ((1 + (2 * (|.py.| * |.py.|))) + (sqrt (1 + (4 * (|.py.| * |.py.|)))))) * ((1 - (sqrt (1 + (4 * (|.py.| * |.py.|))))) / (1 - (sqrt (1 + (4 * (|.py.| * |.py.|)))))) by A12, XCMPLX_1:60 .= ((1 + (sqrt (1 + (4 * (|.py.| * |.py.|))))) * (1 - (sqrt (1 + (4 * (|.py.| * |.py.|)))))) / ((1 - (sqrt (1 + (4 * (|.py.| * |.py.|))))) * ((1 + (2 * (|.py.| * |.py.|))) + (sqrt (1 + (4 * (|.py.| * |.py.|)))))) by XCMPLX_1:76 .= (1 - ((sqrt (1 + (4 * (|.py.| * |.py.|)))) ^2)) / (((1 + (2 * (|.py.| * |.py.|))) - ((2 * (|.py.| * |.py.|)) * (sqrt (1 + (4 * (|.py.| * |.py.|)))))) - ((sqrt (1 + (4 * (|.py.| * |.py.|)))) * (sqrt (1 + (4 * (|.py.| * |.py.|)))))) .= (1 - (1 + (4 * (|.py.| * |.py.|)))) / (((1 + (2 * (|.py.| * |.py.|))) - ((2 * (|.py.| * |.py.|)) * (sqrt (1 + (4 * (|.py.| * |.py.|)))))) - ((sqrt (1 + (4 * (|.py.| * |.py.|)))) ^2)) by SQUARE_1:def_2 .= (- (4 * (|.py.| * |.py.|))) / (((1 + (2 * (|.py.| * |.py.|))) - ((2 * (|.py.| * |.py.|)) * (sqrt (1 + (4 * (|.py.| * |.py.|)))))) - (1 + (4 * (|.py.| * |.py.|)))) by SQUARE_1:def_2 .= (- (4 * (|.py.| * |.py.|))) / ((- (2 * (|.py.| * |.py.|))) * (1 + (sqrt (1 + (4 * (|.py.| * |.py.|)))))) .= ((2 * (- (2 * (|.py.| * |.py.|)))) / (- (2 * (|.py.| * |.py.|)))) / (1 + (sqrt (1 + (4 * (|.py.| * |.py.|))))) by XCMPLX_1:78 .= (2 * ((- (2 * (|.py.| * |.py.|))) / (- (2 * (|.py.| * |.py.|))))) / (1 + (sqrt (1 + (4 * (|.py.| * |.py.|))))) .= (2 * 1) / (1 + (sqrt (1 + (4 * (|.py.| * |.py.|))))) by A7, XCMPLX_1:60 .= 2 / (1 + (sqrt (1 + (4 * (|.py.| * |.py.|))))) ; f . ((2 / (1 + (sqrt (1 + (4 * (|.py.| * |.py.|)))))) * py) = (1 / (1 - (|.((2 / (1 + (sqrt (1 + (4 * (|.py.| * |.py.|)))))) * py).| * |.((2 / (1 + (sqrt (1 + (4 * (|.py.| * |.py.|)))))) * py).|))) * ((2 / (1 + (sqrt (1 + (4 * (|.py.| * |.py.|)))))) * py) by A2, A10 .= (r / r) * py by A13, EUCLID:30 .= 1 * py by A8, XCMPLX_1:60 .= py by EUCLID:29 ; hence [((2 / (1 + (sqrt (1 + (4 * (|.py.| * |.py.|)))))) * py),y] in f by A10, FUNCT_1:def_2; ::_thesis: verum end; end; end; then A14: rng f = [#] (TOP-REAL n1) by RELSET_1:10; 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 ; ::_thesis: ( x1 in dom f & x2 in dom f & f . x1 = f . x2 implies x1 = x2 ) A15: [#] (Tunit_ball n) c= [#] (TOP-REAL n) by PRE_TOPC:def_4; assume A16: x1 in dom f ; ::_thesis: ( not x2 in dom f or not f . x1 = f . x2 or x1 = x2 ) 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 ; ::_thesis: ( not f . x1 = f . x2 or x1 = x2 ) 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 ; ::_thesis: x1 = x2 A20: (1 / (1 - (|.px1.| * |.px1.|))) * px1 = f . x2 by A19, A16, A2 .= (1 / (1 - (|.px2.| * |.px2.|))) * px2 by A17, A2 ; percases ( |.px1.| = 0 or |.px1.| <> 0 ) ; supposeA21: |.px1.| = 0 ; ::_thesis: x1 = x2 then A22: px1 = 0. (TOP-REAL n) by EUCLID_2:42; percases ( 1 / (1 - (|.px2.| * |.px2.|)) = 0 or px2 = 0. (TOP-REAL n) ) by A22, A20, EUCLID:28, EUCLID:31; suppose 1 / (1 - (|.px2.| * |.px2.|)) = 0 ; ::_thesis: x1 = x2 then 1 - (|.px2.| * |.px2.|) = 0 ; then sqrt (|.px2.| ^2) = 1 by SQUARE_1:18; then A23: |.px2.| = 1 by SQUARE_1:22; px2 in Ball ((0. (TOP-REAL n)),1) by A18, Th4; then consider p2 being Point of (TOP-REAL n) such that A24: ( p2 = px2 & |.(p2 - (0. (TOP-REAL n))).| < 1 ) ; thus x1 = x2 by A23, A24, RLVECT_1:13; ::_thesis: verum end; suppose px2 = 0. (TOP-REAL n) ; ::_thesis: x1 = x2 hence x1 = x2 by A21, EUCLID_2:42; ::_thesis: verum end; end; end; supposeA25: |.px1.| <> 0 ; ::_thesis: x1 = x2 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 A26: (- (|.px1.| * |.px1.|)) + 1 > (- 1) + 1 by XREAL_1:6; A27: px1 = 1 * px1 by EUCLID:29 .= ((1 - (|.px1.| * |.px1.|)) / (1 - (|.px1.| * |.px1.|))) * px1 by A26, XCMPLX_1:60 .= (1 - (|.px1.| * |.px1.|)) * ((1 / (1 - (|.px1.| * |.px1.|))) * px1) by EUCLID:30 .= ((1 - (|.px1.| * |.px1.|)) / (1 - (|.px2.| * |.px2.|))) * px2 by A20, EUCLID:30 ; A28: px2 <> 0. (TOP-REAL n1) proof assume px2 = 0. (TOP-REAL n1) ; ::_thesis: contradiction then px1 = 0. (TOP-REAL n1) by A27, EUCLID:28; hence contradiction by A25, TOPRNS_1:23; ::_thesis: verum end; then A29: |.px2.| <> 0 by EUCLID_2:42; px2 in Ball ((0. (TOP-REAL n)),1) by A18, Th4; then consider p2 being Point of (TOP-REAL n) such that A30: ( p2 = px2 & |.(p2 - (0. (TOP-REAL n))).| < 1 ) ; A31: |.px2.| < 1 by A30, RLVECT_1:13; then |.px2.| * |.px2.| < 1 * |.px2.| by A29, XREAL_1:68; then |.px2.| * |.px2.| < 1 by A31, XXREAL_0:2; then - (|.px2.| * |.px2.|) > - 1 by XREAL_1:24; then A32: (- (|.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.|))) * ((1 - (|.px1.| * |.px1.|)) / (1 - (|.px2.| * |.px2.|)))) * px2 by A27, A20, EUCLID:30; then ((1 / (1 - (|.px2.| * |.px2.|))) * px2) - (((1 / (1 - (|.px1.| * |.px1.|))) * ((1 - (|.px1.| * |.px1.|)) / (1 - (|.px2.| * |.px2.|)))) * px2) = 0. (TOP-REAL n) by EUCLID:36; then ((1 / (1 - (|.px2.| * |.px2.|))) * px2) + ((- ((1 / (1 - (|.px1.| * |.px1.|))) * ((1 - (|.px1.| * |.px1.|)) / (1 - (|.px2.| * |.px2.|))))) * px2) = 0. (TOP-REAL n) by EUCLID:40; then A33: ((1 / (1 - (|.px2.| * |.px2.|))) + (- ((1 / (1 - (|.px1.| * |.px1.|))) * ((1 - (|.px1.| * |.px1.|)) / (1 - (|.px2.| * |.px2.|)))))) * px2 = 0. (TOP-REAL n) by EUCLID:33; A34: ((1 - (|.px1.| * |.px1.|)) / (1 - (|.px2.| * |.px2.|))) * ((1 - (|.px1.| * |.px1.|)) / (1 - (|.px2.| * |.px2.|))) = (abs ((1 - (|.px1.| * |.px1.|)) / (1 - (|.px2.| * |.px2.|)))) * (abs ((1 - (|.px1.| * |.px1.|)) / (1 - (|.px2.| * |.px2.|)))) proof percases ( abs ((1 - (|.px1.| * |.px1.|)) / (1 - (|.px2.| * |.px2.|))) = (1 - (|.px1.| * |.px1.|)) / (1 - (|.px2.| * |.px2.|)) or abs ((1 - (|.px1.| * |.px1.|)) / (1 - (|.px2.| * |.px2.|))) = - ((1 - (|.px1.| * |.px1.|)) / (1 - (|.px2.| * |.px2.|))) ) by ABSVALUE:1; suppose abs ((1 - (|.px1.| * |.px1.|)) / (1 - (|.px2.| * |.px2.|))) = (1 - (|.px1.| * |.px1.|)) / (1 - (|.px2.| * |.px2.|)) ; ::_thesis: ((1 - (|.px1.| * |.px1.|)) / (1 - (|.px2.| * |.px2.|))) * ((1 - (|.px1.| * |.px1.|)) / (1 - (|.px2.| * |.px2.|))) = (abs ((1 - (|.px1.| * |.px1.|)) / (1 - (|.px2.| * |.px2.|)))) * (abs ((1 - (|.px1.| * |.px1.|)) / (1 - (|.px2.| * |.px2.|)))) hence ((1 - (|.px1.| * |.px1.|)) / (1 - (|.px2.| * |.px2.|))) * ((1 - (|.px1.| * |.px1.|)) / (1 - (|.px2.| * |.px2.|))) = (abs ((1 - (|.px1.| * |.px1.|)) / (1 - (|.px2.| * |.px2.|)))) * (abs ((1 - (|.px1.| * |.px1.|)) / (1 - (|.px2.| * |.px2.|)))) ; ::_thesis: verum end; suppose abs ((1 - (|.px1.| * |.px1.|)) / (1 - (|.px2.| * |.px2.|))) = - ((1 - (|.px1.| * |.px1.|)) / (1 - (|.px2.| * |.px2.|))) ; ::_thesis: ((1 - (|.px1.| * |.px1.|)) / (1 - (|.px2.| * |.px2.|))) * ((1 - (|.px1.| * |.px1.|)) / (1 - (|.px2.| * |.px2.|))) = (abs ((1 - (|.px1.| * |.px1.|)) / (1 - (|.px2.| * |.px2.|)))) * (abs ((1 - (|.px1.| * |.px1.|)) / (1 - (|.px2.| * |.px2.|)))) hence ((1 - (|.px1.| * |.px1.|)) / (1 - (|.px2.| * |.px2.|))) * ((1 - (|.px1.| * |.px1.|)) / (1 - (|.px2.| * |.px2.|))) = (abs ((1 - (|.px1.| * |.px1.|)) / (1 - (|.px2.| * |.px2.|)))) * (abs ((1 - (|.px1.| * |.px1.|)) / (1 - (|.px2.| * |.px2.|)))) ; ::_thesis: verum end; end; end; (1 / (1 - (|.px2.| * |.px2.|))) + (- ((1 / (1 - (|.px1.| * |.px1.|))) * ((1 - (|.px1.| * |.px1.|)) / (1 - (|.px2.| * |.px2.|))))) = 0 by A28, A33, EUCLID:31; then 1 / (1 - (|.px2.| * |.px2.|)) = (1 * ((1 - (|.px1.| * |.px1.|)) / (1 - (|.px2.| * |.px2.|)))) / (1 - (|.px1.| * |.px1.|)) .= 1 / ((1 - (|.px1.| * |.px1.|)) / ((1 - (|.px1.| * |.px1.|)) / (1 - (|.px2.| * |.px2.|)))) by XCMPLX_1:77 ; then 1 - (|.px2.| * |.px2.|) = (1 - (|.px1.| * |.px1.|)) / ((1 - (|.px1.| * |.px1.|)) / (1 - (|.px2.| * |.px2.|))) by XCMPLX_1:59; then ((1 - (|.px1.| * |.px1.|)) / (1 - (|.px2.| * |.px2.|))) * (1 - (|.px2.| * |.px2.|)) = (1 - (|.px1.| * |.px1.|)) / (((1 - (|.px1.| * |.px1.|)) / (1 - (|.px2.| * |.px2.|))) / ((1 - (|.px1.| * |.px1.|)) / (1 - (|.px2.| * |.px2.|)))) by XCMPLX_1:81 .= (1 - (|.px1.| * |.px1.|)) / 1 by A26, A32, XCMPLX_1:60 .= 1 - (((abs ((1 - (|.px1.| * |.px1.|)) / (1 - (|.px2.| * |.px2.|)))) * |.px2.|) * |.(((1 - (|.px1.| * |.px1.|)) / (1 - (|.px2.| * |.px2.|))) * px2).|) by A27, TOPRNS_1:7 .= 1 - (((abs ((1 - (|.px1.| * |.px1.|)) / (1 - (|.px2.| * |.px2.|)))) * |.px2.|) * ((abs ((1 - (|.px1.| * |.px1.|)) / (1 - (|.px2.| * |.px2.|)))) * |.px2.|)) by TOPRNS_1:7 .= 1 - ((((abs ((1 - (|.px1.| * |.px1.|)) / (1 - (|.px2.| * |.px2.|)))) * (abs ((1 - (|.px1.| * |.px1.|)) / (1 - (|.px2.| * |.px2.|))))) * |.px2.|) * |.px2.|) .= 1 - (((((1 - (|.px1.| * |.px1.|)) / (1 - (|.px2.| * |.px2.|))) * ((1 - (|.px1.| * |.px1.|)) / (1 - (|.px2.| * |.px2.|)))) * |.px2.|) * |.px2.|) by A34 ; then (1 + ((((1 - (|.px1.| * |.px1.|)) / (1 - (|.px2.| * |.px2.|))) * |.px2.|) * |.px2.|)) * (1 - ((1 - (|.px1.| * |.px1.|)) / (1 - (|.px2.| * |.px2.|)))) = 0 ; then 1 - ((1 - (|.px1.| * |.px1.|)) / (1 - (|.px2.| * |.px2.|))) = 0 by A26, A32; hence x1 = x2 by A27, EUCLID:29; ::_thesis: verum end; end; end; then A35: f is one-to-one by FUNCT_1:def_4; consider f0 being 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:20; consider f1 being 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:84; consider f2 being Function of (TOP-REAL n),R^1 such that A38: ( ( for p being Point of (TOP-REAL n) for r1 being real number st f1 . p = r1 holds f2 . p = r1 * r1 ) & f2 is continuous ) by A37, JGRAPH_2:22; consider f3 being Function of (TOP-REAL n),R^1 such that A39: ( ( for p being Point of (TOP-REAL n) for 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:21; reconsider f3 = 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); ::_thesis: f3 . p = 1 - (|.p.| * |.p.|) 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 ; ::_thesis: verum end; set f4 = f3 | (Tunit_ball n); for p being Point of (Tunit_ball n) holds (f3 | (Tunit_ball n)) . p <> 0 proof let p be Point of (Tunit_ball n); ::_thesis: (f3 | (Tunit_ball n)) . p <> 0 assume (f3 | (Tunit_ball n)) . p = 0 ; ::_thesis: contradiction then A41: f3 . p = 0 by FUNCT_1:49; 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; percases ( |.p1.| = 0 or |.p1.| <> 0 ) ; suppose |.p1.| = 0 ; ::_thesis: contradiction hence contradiction by A42; ::_thesis: verum end; suppose |.p1.| <> 0 ; ::_thesis: contradiction then |.p1.| * |.p1.| < 1 * |.p1.| by Th5, XREAL_1:68; hence contradiction by A42, Th5; ::_thesis: verum end; end; end; then consider f5 being Function of (Tunit_ball n),R^1 such that A43: ( ( for p being Point of (Tunit_ball n) for r1 being real number st (f3 | (Tunit_ball n)) . p = r1 holds f5 . p = 1 / r1 ) & f5 is continuous ) by JGRAPH_2:26; consider f6 being Function of (Tunit_ball n),(TOP-REAL n) such that A44: ( ( for a being Point of (Tunit_ball n) for b being Point of (TOP-REAL n) for 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 ; ::_thesis: ( x in dom f implies f . x = f6 . x ) assume A46: x in dom f ; ::_thesis: f . x = f6 . x 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; (f3 | (Tunit_ball n)) . p = f3 . p by A46, FUNCT_1:49 .= 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; ::_thesis: verum end; then A48: f = f6 by A45, FUNCT_1:2; consider f8 being Function of (TOP-REAL n),R^1 such that A49: ( ( for p being Point of (TOP-REAL n) for r1 being real number st f2 . p = r1 holds f8 . p = 4 * r1 ) & f8 is continuous ) by A38, JGRAPH_2:23; consider f9 being Function of (TOP-REAL n),R^1 such that A50: ( ( for p being Point of (TOP-REAL n) for 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:19; 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); ::_thesis: f9 . p = 1 + ((4 * |.p.|) * |.p.|) 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.|) ; ::_thesis: verum 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); ::_thesis: ex r being real number st ( f9 . p = r & r >= 0 ) set r = 1 + ((4 * |.p.|) * |.p.|); take 1 + ((4 * |.p.|) * |.p.|) ; ::_thesis: ( f9 . p = 1 + ((4 * |.p.|) * |.p.|) & 1 + ((4 * |.p.|) * |.p.|) >= 0 ) thus ( f9 . p = 1 + ((4 * |.p.|) * |.p.|) & 1 + ((4 * |.p.|) * |.p.|) >= 0 ) by A51; ::_thesis: verum end; consider f10 being Function of (TOP-REAL n),R^1 such that A53: ( ( for p being Point of (TOP-REAL n) for r1 being real number st f9 . p = r1 holds f10 . p = sqrt r1 ) & f10 is continuous ) by A52, A50, JGRAPH_3:5; consider f11 being Function of (TOP-REAL n),R^1 such that A54: ( ( for p being Point of (TOP-REAL n) for 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:19; for p being Point of (TOP-REAL n) holds f11 . p <> 0 proof let p be Point of (TOP-REAL n); ::_thesis: f11 . p <> 0 A55: f11 . p = (f0 . p) + (f10 . p) by A54 .= 1 + (f10 . p) by A36 .= 1 + (sqrt (f9 . p)) by A53 ; consider r being real number such that A56: ( r = f9 . p & r >= 0 ) by A52; sqrt (f9 . p) >= 0 by A56, SQUARE_1:def_2; hence f11 . p <> 0 by A55; ::_thesis: verum end; then consider f12 being Function of (TOP-REAL n),R^1 such that A57: ( ( for p being Point of (TOP-REAL n) for r1 being real number st f11 . p = r1 holds f12 . p = 1 / r1 ) & f12 is continuous ) by A54, JGRAPH_2:26; consider f13 being Function of (TOP-REAL n),R^1 such that A58: ( ( for p being Point of (TOP-REAL n) for r1 being real number st f12 . p = r1 holds f13 . p = 2 * r1 ) & f13 is continuous ) by A57, JGRAPH_2:23; 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); ::_thesis: f13 . p = 2 / (1 + (sqrt (1 + ((4 * |.p.|) * |.p.|)))) 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 ; ::_thesis: verum end; reconsider X = TOP-REAL n as non empty SubSpace of TOP-REAL n by TSEP_1:2; consider f14 being Function of X,(TOP-REAL n) such that A60: ( ( for a being Point of X for b being Point of (TOP-REAL n) for r being real number st a = b & f13 . a = r holds f14 . b = r * b ) & f14 is continuous ) by A58, Th2; reconsider f14 = 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 ; ::_thesis: (abs r) * (abs r) = r * r percases ( abs r = r or abs r = - r ) by ABSVALUE:1; suppose abs r = r ; ::_thesis: (abs r) * (abs r) = r * r hence (abs r) * (abs r) = r * r ; ::_thesis: verum end; suppose abs r = - r ; ::_thesis: (abs r) * (abs r) = r * r hence (abs r) * (abs r) = r * r ; ::_thesis: verum end; 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 ; ::_thesis: ( y in the carrier of (Tunit_ball n) iff ex x being set st ( x in dom f14 & y = f14 . x ) ) hereby ::_thesis: ( ex x being set st ( x in dom f14 & y = f14 . x ) implies y in the carrier of (Tunit_ball n) ) assume A63: y in the carrier of (Tunit_ball n) ; ::_thesis: ex x being set st ( x in dom f14 & f14 . x = y ) [#] (Tunit_ball n) c= [#] (TOP-REAL n) by PRE_TOPC:def_4; 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:64; then |.q.| * |.q.| < 1 by A63, Th5, XXREAL_0:2; then A64: 0 < 1 - (|.q.| * |.q.|) by XREAL_1:50; set p = (1 / (1 - (|.q.| * |.q.|))) * q; |.((1 / (1 - (|.q.| * |.q.|))) * q).| = (abs (1 / (1 - (|.q.| * |.q.|)))) * |.q.| by TOPRNS_1:7; then |.((1 / (1 - (|.q.| * |.q.|))) * q).| * |.((1 / (1 - (|.q.| * |.q.|))) * q).| = (((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:76 .= (|.q.| * |.q.|) / ((1 - (|.q.| * |.q.|)) * (1 - (|.q.| * |.q.|))) ; then A65: 1 + ((4 * |.((1 / (1 - (|.q.| * |.q.|))) * q).|) * |.((1 / (1 - (|.q.| * |.q.|))) * q).|) = (((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:76 ; sqrt (1 + ((4 * |.((1 / (1 - (|.q.| * |.q.|))) * q).|) * |.((1 / (1 - (|.q.| * |.q.|))) * q).|)) = (1 + (|.q.| * |.q.|)) / (1 - (|.q.| * |.q.|)) by A64, A65, SQUARE_1:22; then A66: 1 + (sqrt (1 + ((4 * |.((1 / (1 - (|.q.| * |.q.|))) * q).|) * |.((1 / (1 - (|.q.| * |.q.|))) * q).|))) = ((1 - (|.q.| * |.q.|)) / (1 - (|.q.| * |.q.|))) + ((1 + (|.q.| * |.q.|)) / (1 - (|.q.| * |.q.|))) by A64, XCMPLX_1:60 .= 2 / (1 - (|.q.| * |.q.|)) ; reconsider x = (1 / (1 - (|.q.| * |.q.|))) * q as set ; take x = x; ::_thesis: ( x in dom f14 & f14 . x = y ) thus x in dom f14 by A61; ::_thesis: f14 . x = y thus f14 . x = (f13 . ((1 / (1 - (|.q.| * |.q.|))) * q)) * ((1 / (1 - (|.q.| * |.q.|))) * q) by A60 .= (2 / (2 / (1 - (|.q.| * |.q.|)))) * ((1 / (1 - (|.q.| * |.q.|))) * q) by A66, A59 .= (1 - (|.q.| * |.q.|)) * ((1 / (1 - (|.q.| * |.q.|))) * q) by XCMPLX_1:52 .= ((1 - (|.q.| * |.q.|)) / (1 - (|.q.| * |.q.|))) * q by EUCLID:30 .= 1 * q by A64, XCMPLX_1:60 .= y by EUCLID:29 ; ::_thesis: verum end; given x being set such that A67: ( x in dom f14 & y = f14 . x ) ; ::_thesis: y in the carrier of (Tunit_ball n) reconsider p = x as Point of (TOP-REAL n1) by A67; y in rng f14 by A67, FUNCT_1:3; 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:7; 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 ; ::_thesis: contradiction then A69: (((2 * 2) / ((1 + (sqrt (1 + ((4 * |.p.|) * |.p.|)))) * (1 + (sqrt (1 + ((4 * |.p.|) * |.p.|)))))) * |.p.|) * |.p.| >= 1 by A68, 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 A69, 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; ::_thesis: verum end; then |.q.| ^2 < 1 ; then A70: |.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 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_5; hence y in the carrier of (Tunit_ball n) ; ::_thesis: verum end; then A71: rng f14 = the carrier of (Tunit_ball n) by FUNCT_1:def_3; then reconsider f14 = f14 as Function of (TOP-REAL n),(Tunit_ball n) by A61, FUNCT_2:1; 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 ; ::_thesis: ( x in dom f14 implies f14 . x = (f ") . x ) assume A73: x in dom f14 ; ::_thesis: f14 . x = (f ") . x reconsider g = f as Function ; f is onto by A14, FUNCT_2:def_3; then A74: f " = g " by A35, TOPS_2:def_4; A75: f14 . x in rng f14 by A73, FUNCT_1:3; 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_2; |.q.| = (abs (2 / (1 + (sqrt (1 + ((4 * |.p.|) * |.p.|)))))) * |.p.| by A77, TOPRNS_1:7; 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:76 .= ((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_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 A78, XCMPLX_1:91 ; 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:30 .= ((2 * (1 + (sqrt (1 + ((4 * |.p.|) * |.p.|))))) / (2 * (1 + (sqrt (1 + ((4 * |.p.|) * |.p.|)))))) * p by XCMPLX_1:76 .= 1 * p by A78, XCMPLX_1:60 .= p by EUCLID:29 ; then [(f14 . x),x] in f by A76, FUNCT_1:def_2; then [x,(f14 . x)] in g ~ by RELAT_1:def_7; then [x,(f14 . x)] in g " by A35, FUNCT_1:def_5; hence f14 . x = (f ") . x by A74, FUNCT_1:1; ::_thesis: verum end; then f " is continuous by A72, FUNCT_1:2, PRE_TOPC:27; hence f is being_homeomorphism by A3, A14, A35, A44, A48, TOPS_2:def_5; ::_thesis: verum end; theorem Th7: :: MFOLD_1:7 for n being Nat for p being Point of (TOP-REAL n) for r being real positive number for f being Function of (Tunit_ball n),(Tball (p,r)) st n <> 0 & ( for a being Point of (Tunit_ball n) for b being Point of (TOP-REAL n) st a = b holds f . a = (r * b) + p ) holds f is being_homeomorphism proof let n be Nat; ::_thesis: for p being Point of (TOP-REAL n) for r being real positive number for f being Function of (Tunit_ball n),(Tball (p,r)) st n <> 0 & ( for a being Point of (Tunit_ball n) for b being Point of (TOP-REAL n) st a = b holds f . a = (r * b) + p ) holds f is being_homeomorphism let p be Point of (TOP-REAL n); ::_thesis: for r being real positive number for f being Function of (Tunit_ball n),(Tball (p,r)) st n <> 0 & ( for a being Point of (Tunit_ball n) for b being Point of (TOP-REAL n) st a = b holds f . a = (r * b) + p ) holds f is being_homeomorphism let r be real positive number ; ::_thesis: for f being Function of (Tunit_ball n),(Tball (p,r)) st n <> 0 & ( for a being Point of (Tunit_ball n) for b being Point of (TOP-REAL n) st a = b holds f . a = (r * b) + p ) holds f is being_homeomorphism let f be Function of (Tunit_ball n),(Tball (p,r)); ::_thesis: ( n <> 0 & ( for a being Point of (Tunit_ball n) for b being Point of (TOP-REAL n) st a = b holds f . a = (r * b) + p ) implies f is being_homeomorphism ) assume that A1: n <> 0 and A2: for a being Point of (Tunit_ball n) for b being Point of (TOP-REAL n) st a = b holds f . a = (r * b) + p ; ::_thesis: f is being_homeomorphism reconsider n1 = n as non empty Element of NAT by A1, ORDINAL1:def_12; reconsider x = p as Point of (TOP-REAL n1) ; defpred S1[ Point of (TOP-REAL n1), set ] means $2 = (r * $1) + x; set U = Tunit_ball n; set B = Tball (x,r); A3: for u being Point of (TOP-REAL n1) ex y being Point of (TOP-REAL n1) st S1[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 S1[x,F . x] from FUNCT_2:sch_3(A3); defpred S2[ 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 S2[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 S2[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 being Point of (TOP-REAL n1) holds G . p = ((1 / r) * ((id (TOP-REAL n1)) . p)) + ((- (1 / r)) * (((TOP-REAL n1) --> x) . p)) proof let p be Point of (TOP-REAL n1); ::_thesis: G . p = ((1 / r) * ((id (TOP-REAL n1)) . p)) + ((- (1 / r)) * (((TOP-REAL n1) --> x) . p)) thus ((1 / r) * ((id (TOP-REAL n1)) . p)) + ((- (1 / r)) * (((TOP-REAL n1) --> x) . p)) = ((1 / r) * p) + ((- (1 / r)) * (((TOP-REAL n1) --> x) . p)) by FUNCT_1:18 .= ((1 / r) * p) + ((- (1 / r)) * x) by FUNCOP_1:7 .= ((1 / r) * p) - ((1 / r) * x) by EUCLID:40 .= (1 / r) * (p - x) by EUCLID:49 .= G . p by A6 ; ::_thesis: verum end; then A8: G is continuous by TOPALG_1:16; A9: dom f = [#] (Tunit_ball n) by FUNCT_2:def_1; A10: dom f = the carrier of (Tunit_ball n) by FUNCT_2:def_1; for p being Point of (TOP-REAL n1) holds F . p = (r * ((id (TOP-REAL n1)) . p)) + (1 * (((TOP-REAL n1) --> x) . p)) proof let p be Point of (TOP-REAL n1); ::_thesis: F . p = (r * ((id (TOP-REAL n1)) . p)) + (1 * (((TOP-REAL n1) --> x) . p)) thus (r * ((id (TOP-REAL n1)) . p)) + (1 * (((TOP-REAL n1) --> x) . p)) = (r * ((id (TOP-REAL n1)) . p)) + (((TOP-REAL n1) --> x) . p) by EUCLID:29 .= (r * p) + (((TOP-REAL n1) --> x) . p) by FUNCT_1:18 .= (r * p) + x by FUNCOP_1:7 .= F . p by A4 ; ::_thesis: verum end; then A11: F is continuous by TOPALG_1:16; A12: the carrier of (Tball (x,r)) = Ball (x,r) by Th4; A13: the carrier of (Tunit_ball n) = 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 ; ::_thesis: ( a in dom f implies f . a = (F | (Ball ((0. (TOP-REAL n)),1))) . a ) assume A15: a in dom f ; ::_thesis: f . a = (F | (Ball ((0. (TOP-REAL n)),1))) . a 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 ; ::_thesis: verum end; A16: (1 / r) * r = 1 by XCMPLX_1:87; A17: rng f = [#] (Tball (x,r)) proof now__::_thesis:_for_b_being_set_st_b_in_[#]_(Tball_(x,r))_holds_ b_in_rng_f let b be set ; ::_thesis: ( b in [#] (Tball (x,r)) implies b in rng f ) assume A18: b in [#] (Tball (x,r)) ; ::_thesis: b in rng f 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: |.((r1 * (c - x)) - (0. (TOP-REAL n1))).| = |.(r1 * (c - x)).| by RLVECT_1:13 .= (abs r1) * |.(c - x).| by TOPRNS_1:7 .= 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:68; then A20: r1 * (c - x) in Ball ((0. (TOP-REAL n)),1) by A16, A19; then f . (r1 * (c - x)) = (r * (r1 * (c - x))) + x by A2, A13 .= ((r * (1 / r)) * (c - x)) + x by EUCLID:30 .= (c - x) + x by A16, EUCLID:29 .= b by EUCLID:48 ; hence b in rng f by A13, A10, A20, FUNCT_1:def_3; ::_thesis: verum end; then [#] (Tball (x,r)) c= rng f by TARSKI:def_3; hence rng f = [#] (Tball (x,r)) by XBOOLE_0:def_10; ::_thesis: verum end; now__::_thesis:_for_a,_b_being_set_st_a_in_dom_f_&_b_in_dom_f_&_f_._a_=_f_._b_holds_ a_=_b let a, b be set ; ::_thesis: ( a in dom f & b in dom f & f . a = f . b implies a = b ) assume that A21: a in dom f and A22: b in dom f and A23: f . a = f . b ; ::_thesis: a = 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:48; hence a = b by EUCLID:34, EUCLID:48; ::_thesis: verum end; then A25: f is one-to-one by FUNCT_1:def_4; 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 ; ::_thesis: ( a in dom (f ") implies (f ") . a = (G | (Ball (x,r))) . a ) assume A27: a in dom (f ") ; ::_thesis: (f ") . a = (G | (Ball (x,r))) . a 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: |.(((1 / r) * (y - x)) - (0. (TOP-REAL n1))).| = |.((1 / r) * (y - x)).| by RLVECT_1:13 .= (abs r1) * |.(y - x).| by TOPRNS_1:7 .= 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:68; then A30: (1 / r) * (y - x) in Ball ((0. (TOP-REAL n)),1) by A16, A29; then f . ((1 / r) * (y - x)) = (r * ((1 / r) * (y - x))) + x by A2, A13 .= ((r * (1 / r)) * (y - x)) + x by EUCLID:30 .= (y - x) + x by A16, EUCLID:29 .= y by EUCLID:48 ; 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 ; ::_thesis: verum 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 (Tball (x,r)) by FUNCT_2:def_1; f " is continuous by A32, A12, A7, A8, A26, BORSUK_4:44, FUNCT_1:2; hence f is being_homeomorphism by A9, A17, A25, A31, TOPS_2:def_5; ::_thesis: verum end; theorem Th8: :: MFOLD_1:8 for n being Nat holds Tunit_ball n, TOP-REAL n are_homeomorphic proof let n be Nat; ::_thesis: Tunit_ball n, TOP-REAL n are_homeomorphic reconsider n1 = n as Element of NAT by ORDINAL1:def_12; set U = Tunit_ball n; set C = TOP-REAL n; percases ( not n is empty or n is empty ) ; supposeA1: not n is empty ; ::_thesis: Tunit_ball n, TOP-REAL n are_homeomorphic defpred S1[ Point of (Tunit_ball n), 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 (Tunit_ball n) ex y being Point of (TOP-REAL n) st S1[u,y] proof let u be Point of (Tunit_ball n); ::_thesis: ex y being Point of (TOP-REAL n) st S1[u,y] reconsider v = u as Point of (TOP-REAL n1) by PRE_TOPC:25; set y = (1 / (1 - (|.v.| * |.v.|))) * v; reconsider y = (1 / (1 - (|.v.| * |.v.|))) * v as Point of (TOP-REAL n) ; take y ; ::_thesis: S1[u,y] thus S1[u,y] ; ::_thesis: verum end; consider f being Function of (Tunit_ball n),(TOP-REAL n) such that A3: for x being Point of (Tunit_ball n) holds S1[x,f . x] from FUNCT_2:sch_3(A2); for a being Point of (Tunit_ball n) for b being Point of (TOP-REAL n1) st a = b holds f . a = (1 / (1 - (|.b.| * |.b.|))) * b proof let a be Point of (Tunit_ball n); ::_thesis: for b being Point of (TOP-REAL n1) st a = b holds f . a = (1 / (1 - (|.b.| * |.b.|))) * b let b be Point of (TOP-REAL n1); ::_thesis: ( a = b implies f . a = (1 / (1 - (|.b.| * |.b.|))) * b ) S1[a,f . a] by A3; hence ( a = b implies f . a = (1 / (1 - (|.b.| * |.b.|))) * b ) ; ::_thesis: verum end; then ex f being Function of (Tunit_ball n),(TOP-REAL n) st f is being_homeomorphism by A1, Th6; hence Tunit_ball n, TOP-REAL n are_homeomorphic by T_0TOPSP:def_1; ::_thesis: verum end; supposeA4: n is empty ; ::_thesis: Tunit_ball n, TOP-REAL n are_homeomorphic 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 ; ::_thesis: ( x in Ball ((0. (TOP-REAL 0)),1) iff x = 0. (TOP-REAL 0) ) thus ( x in Ball ((0. (TOP-REAL 0)),1) implies x = 0. (TOP-REAL 0) ) ; ::_thesis: ( x = 0. (TOP-REAL 0) implies x in Ball ((0. (TOP-REAL 0)),1) ) assume x = 0. (TOP-REAL 0) ; ::_thesis: x in Ball ((0. (TOP-REAL 0)),1) 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) ; ::_thesis: verum 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 Tunit_ball n, TOP-REAL n are_homeomorphic by A4, Th1; ::_thesis: verum end; end; end; theorem Th9: :: MFOLD_1:9 for n being Nat for p, q being Point of (TOP-REAL n) for r, s being real positive number holds Tball (p,r), Tball (q,s) are_homeomorphic proof let n be Nat; ::_thesis: for p, q being Point of (TOP-REAL n) for r, s being real positive number holds Tball (p,r), Tball (q,s) are_homeomorphic let p, q be Point of (TOP-REAL n); ::_thesis: for r, s being real positive number holds Tball (p,r), Tball (q,s) are_homeomorphic let r, s be real positive number ; ::_thesis: Tball (p,r), Tball (q,s) are_homeomorphic percases ( n is empty or not n is empty ) ; supposeA1: n is empty ; ::_thesis: Tball (p,r), Tball (q,s) are_homeomorphic reconsider n1 = n as Element of NAT by ORDINAL1:def_12; 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 where x is Point of (TOP-REAL n) : |.(x - p).| < r } iff x in { x where x is Point of (TOP-REAL n) : |.(x - q).| < s } ) proof let x be set ; ::_thesis: ( x in { x where x is Point of (TOP-REAL n) : |.(x - p).| < r } iff x in { x where x is Point of (TOP-REAL n) : |.(x - q).| < s } ) hereby ::_thesis: ( x in { x where x is Point of (TOP-REAL n) : |.(x - q).| < s } implies x in { x where x is Point of (TOP-REAL n) : |.(x - p).| < r } ) assume x in { x where x is Point of (TOP-REAL n) : |.(x - p).| < r } ; ::_thesis: x in { x where x is Point of (TOP-REAL n) : |.(x - q).| < s } then consider x1 being Point of (TOP-REAL n) such that A4: ( x = x1 & |.(x1 - p).| < r ) ; reconsider x1 = x1 as Point of (TOP-REAL n1) ; x1 = 0. (TOP-REAL 0) by A1; then |.(x1 - p1).| = 0 by A2, TOPRNS_1:28; hence x in { x where x is Point of (TOP-REAL n) : |.(x - q).| < s } by A2, A3, A4; ::_thesis: verum end; assume x in { x where x is Point of (TOP-REAL n) : |.(x - q).| < s } ; ::_thesis: x in { x where x is Point of (TOP-REAL n) : |.(x - p).| < r } then consider x1 being Point of (TOP-REAL n) such that A5: ( x = x1 & |.(x1 - q).| < s ) ; reconsider x1 = x1 as Point of (TOP-REAL n1) ; x1 = 0. (TOP-REAL 0) by A1; then |.(x1 - q1).| = 0 by A3, TOPRNS_1:28; hence x in { x where x is Point of (TOP-REAL n) : |.(x - p).| < r } by A2, A3, A5; ::_thesis: verum end; hence Tball (p,r), Tball (q,s) are_homeomorphic by TARSKI:1; ::_thesis: verum end; suppose not n is empty ; ::_thesis: Tball (p,r), Tball (q,s) are_homeomorphic then reconsider n1 = n as non empty Element of NAT by ORDINAL1:def_12; A6: for r being real positive number for x being Point of (TOP-REAL n1) holds Tunit_ball n1, Tball (x,r) are_homeomorphic proof let r be real positive number ; ::_thesis: for x being Point of (TOP-REAL n1) holds Tunit_ball n1, Tball (x,r) are_homeomorphic let x be Point of (TOP-REAL n1); ::_thesis: Tunit_ball n1, Tball (x,r) are_homeomorphic set U = Tunit_ball n; set C = Tball (x,r); defpred S1[ Point of (Tunit_ball n), 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 (Tball (x,r)) = Ball (x,r) by Th4; A9: for u being Point of (Tunit_ball n) ex y being Point of (Tball (x,r)) st S1[u,y] proof let u be Point of (Tunit_ball n); ::_thesis: ex y being Point of (Tball (x,r)) st S1[u,y] reconsider v = u as Point of (TOP-REAL n1) by PRE_TOPC:25; set y = (r * v) + x; A10: |.(((r * v) + x) - x).| = |.(r * v).| by EUCLID:48 .= (abs r) * |.v.| by A7, TOPRNS_1:7 .= r * |.v.| by ABSVALUE:def_1 ; r * |.v.| < r * 1 by Th5, XREAL_1:68; then reconsider y = (r * v) + x as Point of (Tball (x,r)) by A10, A8, TOPREAL9:7; take y ; ::_thesis: S1[u,y] thus S1[u,y] ; ::_thesis: verum end; consider f being Function of (Tunit_ball n),(Tball (x,r)) such that A11: for x being Point of (Tunit_ball n) holds S1[x,f . x] from FUNCT_2:sch_3(A9); for a being Point of (Tunit_ball n) for b being Point of (TOP-REAL n1) st a = b holds f . a = (r * b) + x proof let a be Point of (Tunit_ball n); ::_thesis: for b being Point of (TOP-REAL n1) st a = b holds f . a = (r * b) + x let b be Point of (TOP-REAL n1); ::_thesis: ( a = b implies f . a = (r * b) + x ) S1[a,f . a] by A11; hence ( a = b implies f . a = (r * b) + x ) ; ::_thesis: verum end; then ex f being Function of (Tunit_ball n),(Tball (x,r)) st f is being_homeomorphism by Th7; hence Tunit_ball n1, Tball (x,r) are_homeomorphic by T_0TOPSP:def_1; ::_thesis: verum 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); ::_thesis: Tball (x,r), Tball (y,s) are_homeomorphic A12: Tunit_ball n, Tball (y,s) are_homeomorphic by A6; Tball (x,r), Tunit_ball n are_homeomorphic by A6; hence Tball (x,r), Tball (y,s) are_homeomorphic by A12, BORSUK_3:3; ::_thesis: verum end; hence Tball (p,r), Tball (q,s) are_homeomorphic ; ::_thesis: verum end; end; end; theorem Th10: :: MFOLD_1:10 for n being Nat for B being non empty ball Subset of (TOP-REAL n) holds B, [#] (TOP-REAL n) are_homeomorphic proof let n be Nat; ::_thesis: for B being non empty ball Subset of (TOP-REAL n) holds B, [#] (TOP-REAL n) are_homeomorphic let B be non empty ball Subset of (TOP-REAL n); ::_thesis: B, [#] (TOP-REAL n) are_homeomorphic consider p being Point of (TOP-REAL n), r being 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; ::_thesis: verum end; theorem Th11: :: MFOLD_1:11 for M, N being non empty TopSpace for p being Point of M for U being a_neighborhood of p for B being open Subset of N st U,B are_homeomorphic holds ex V being open Subset of M ex 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; ::_thesis: for p being Point of M for U being a_neighborhood of p for B being open Subset of N st U,B are_homeomorphic holds ex V being open Subset of M ex S being open Subset of N st ( V c= U & p in V & V,S are_homeomorphic ) let p be Point of M; ::_thesis: for U being a_neighborhood of p for B being open Subset of N st U,B are_homeomorphic holds ex V being open Subset of M ex S being open Subset of N st ( V c= U & p in V & V,S are_homeomorphic ) let U be a_neighborhood of p; ::_thesis: for B being open Subset of N st U,B are_homeomorphic holds ex V being open Subset of M ex S being open Subset of N st ( V c= U & p in V & V,S are_homeomorphic ) let B be open Subset of N; ::_thesis: ( U,B are_homeomorphic implies ex V being open Subset of M ex S being open Subset of N st ( V c= U & p in V & V,S are_homeomorphic ) ) assume U,B are_homeomorphic ; ::_thesis: ex V being open Subset of M ex S being open Subset of N st ( V c= U & p in V & V,S are_homeomorphic ) then A1: M | U,N | B are_homeomorphic by METRIZTS:def_1; then consider f being Function of (M | U),(N | B) such that A2: f is being_homeomorphism by T_0TOPSP:def_1; consider V being 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; 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 = 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 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_2; V1 = V /\ ([#] M1) by XBOOLE_1:28; then V1 in the topology of M1 by A7, PRE_TOPC:def_4; then V1 is open by PRE_TOPC:def_2; then S1 is open by A6; then reconsider S = S as open Subset of N by TSEP_1:17; take V ; ::_thesis: ex S being open Subset of N st ( V c= U & p in V & V,S are_homeomorphic ) take S ; ::_thesis: ( V c= U & p in V & V,S are_homeomorphic ) thus ( V c= U & p in V ) by A3; ::_thesis: V,S are_homeomorphic 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, XBOOLE_1:1; 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; ::_thesis: verum end; begin definition let n be Nat; let M be non empty TopSpace; attrM is n -locally_euclidean means :Def4: :: MFOLD_1:def 4 for p being Point of M ex U being a_neighborhood of p ex S being open Subset of (TOP-REAL n) st U,S are_homeomorphic ; end; :: deftheorem Def4 defines -locally_euclidean MFOLD_1:def_4_:_ for n being Nat for M being non empty TopSpace holds ( M is n -locally_euclidean iff for p being Point of M ex U being a_neighborhood of p ex S being open Subset of (TOP-REAL n) st U,S are_homeomorphic ); registration let n be Nat; cluster TOP-REAL n -> n -locally_euclidean ; coherence TOP-REAL n is n -locally_euclidean proof let p be Point of (TOP-REAL n); :: according to MFOLD_1:def_4 ::_thesis: ex U being a_neighborhood of p ex S being open Subset of (TOP-REAL n) st U,S are_homeomorphic 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 ; ::_thesis: ex S being open Subset of (TOP-REAL n) st U,S are_homeomorphic take S ; ::_thesis: U,S are_homeomorphic thus U,S are_homeomorphic by METRIZTS:1; ::_thesis: verum end; end; registration let n be Nat; cluster non empty TopSpace-like n -locally_euclidean for TopStruct ; correctness existence ex b1 being non empty TopSpace st b1 is n -locally_euclidean ; proof take TOP-REAL n ; ::_thesis: TOP-REAL n is n -locally_euclidean thus TOP-REAL n is n -locally_euclidean ; ::_thesis: verum end; end; Lm1: for n being Nat for M being non empty TopSpace st M is n -locally_euclidean holds for p being Point of M ex U being a_neighborhood of p ex B being non empty ball Subset of (TOP-REAL n) st U,B are_homeomorphic proof let n be Nat; ::_thesis: for M being non empty TopSpace st M is n -locally_euclidean holds for p being Point of M ex U being a_neighborhood of p ex B being non empty ball Subset of (TOP-REAL n) st U,B are_homeomorphic let M be non empty TopSpace; ::_thesis: ( M is n -locally_euclidean implies for p being Point of M ex U being a_neighborhood of p ex B being non empty ball Subset of (TOP-REAL n) st U,B are_homeomorphic ) assume A1: M is n -locally_euclidean ; ::_thesis: for p being Point of M ex U being a_neighborhood of p ex B being non empty ball Subset of (TOP-REAL n) st U,B are_homeomorphic let p be Point of M; ::_thesis: ex U being a_neighborhood of p ex B being non empty ball Subset of (TOP-REAL n) st U,B are_homeomorphic consider U being a_neighborhood of p, S being open Subset of (TOP-REAL n) such that A2: U,S are_homeomorphic by A1, Def4; consider U1 being open Subset of M, S being open Subset of (TOP-REAL n) such that A3: ( U1 c= U & p in U1 & U1,S are_homeomorphic ) by A2, Th11; reconsider U1 = 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 being 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_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 = 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 being ball Subset of (TOP-REAL n) such that A9: ( B c= S & q in B ) by A6, A7, Th3, FUNCT_2:5; reconsider B = 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; then reconsider U2 = (f ") .: B1 as non empty Subset of M1 ; 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 = V as a_neighborhood of p by A19, CONNSP_2:3, CONNSP_2:9; take V ; ::_thesis: ex B being non empty ball Subset of (TOP-REAL n) st V,B are_homeomorphic take B ; ::_thesis: V,B are_homeomorphic 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; ::_thesis: verum end; theorem :: MFOLD_1:12 for n being Nat for M being non empty TopSpace holds ( M is n -locally_euclidean iff for p being Point of M ex U being a_neighborhood of p ex B being ball Subset of (TOP-REAL n) st U,B are_homeomorphic ) proof let n be Nat; ::_thesis: for M being non empty TopSpace holds ( M is n -locally_euclidean iff for p being Point of M ex U being a_neighborhood of p ex B being ball Subset of (TOP-REAL n) st U,B are_homeomorphic ) let M be non empty TopSpace; ::_thesis: ( M is n -locally_euclidean iff for p being Point of M ex U being a_neighborhood of p ex B being ball Subset of (TOP-REAL n) st U,B are_homeomorphic ) hereby ::_thesis: ( ( for p being Point of M ex U being a_neighborhood of p ex B being ball Subset of (TOP-REAL n) st U,B are_homeomorphic ) implies M is n -locally_euclidean ) assume A1: M is n -locally_euclidean ; ::_thesis: for p being Point of M ex U being a_neighborhood of p ex B being ball Subset of (TOP-REAL n) st U,B are_homeomorphic let p be Point of M; ::_thesis: ex U being a_neighborhood of p ex B being ball Subset of (TOP-REAL n) st U,B are_homeomorphic consider U being a_neighborhood of p, B being non empty ball Subset of (TOP-REAL n) such that A2: U,B are_homeomorphic by A1, Lm1; reconsider B = B as ball Subset of (TOP-REAL n) ; take U = U; ::_thesis: ex B being ball Subset of (TOP-REAL n) st U,B are_homeomorphic take B = B; ::_thesis: U,B are_homeomorphic thus U,B are_homeomorphic by A2; ::_thesis: verum end; assume A3: for p being Point of M ex U being a_neighborhood of p ex B being ball Subset of (TOP-REAL n) st U,B are_homeomorphic ; ::_thesis: M is n -locally_euclidean now__::_thesis:_for_p_being_Point_of_M_ex_U_being_a_neighborhood_of_p_ex_S_being_open_Subset_of_(TOP-REAL_n)_st_U,S_are_homeomorphic let p be Point of M; ::_thesis: ex U being a_neighborhood of p ex S being open Subset of (TOP-REAL n) st U,S are_homeomorphic consider U being a_neighborhood of p, B being 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 = U; ::_thesis: ex S being open Subset of (TOP-REAL n) st U,S are_homeomorphic take S = S; ::_thesis: U,S are_homeomorphic thus U,S are_homeomorphic by A4; ::_thesis: verum end; hence M is n -locally_euclidean by Def4; ::_thesis: verum end; theorem Th13: :: MFOLD_1:13 for n being Nat for M being non empty TopSpace holds ( M is n -locally_euclidean iff for p being Point of M ex U being a_neighborhood of p st U, [#] (TOP-REAL n) are_homeomorphic ) proof let n be Nat; ::_thesis: for M being non empty TopSpace holds ( M is n -locally_euclidean iff for p being Point of M ex U being a_neighborhood of p st U, [#] (TOP-REAL n) are_homeomorphic ) let M be non empty TopSpace; ::_thesis: ( M is n -locally_euclidean iff for p being Point of M ex U being a_neighborhood of p st U, [#] (TOP-REAL n) are_homeomorphic ) hereby ::_thesis: ( ( for p being Point of M ex U being a_neighborhood of p st U, [#] (TOP-REAL n) are_homeomorphic ) implies M is n -locally_euclidean ) assume A1: M is n -locally_euclidean ; ::_thesis: for p being Point of M ex U being a_neighborhood of p st U, [#] (TOP-REAL n) are_homeomorphic let p be Point of M; ::_thesis: ex U being a_neighborhood of p st U, [#] (TOP-REAL n) are_homeomorphic consider U being a_neighborhood of p, B being non empty ball Subset of (TOP-REAL n) such that A2: U,B are_homeomorphic by A1, Lm1; take U = U; ::_thesis: U, [#] (TOP-REAL n) are_homeomorphic A3: (TOP-REAL n) | ([#] (TOP-REAL n)) = TopStruct(# the carrier of (TOP-REAL n), the topology 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; B, [#] (TOP-REAL n) are_homeomorphic by Th10; then A5: B1, TopStruct(# the carrier of (TOP-REAL n), the topology of (TOP-REAL n) #) are_homeomorphic by A3, METRIZTS:def_1; U1, TopStruct(# the carrier of (TOP-REAL n), the topology of (TOP-REAL n) #) are_homeomorphic by A4, A5, BORSUK_3:3; hence U, [#] (TOP-REAL n) are_homeomorphic by A3, METRIZTS:def_1; ::_thesis: verum end; assume A6: for p being Point of M ex U being a_neighborhood of p st U, [#] (TOP-REAL n) are_homeomorphic ; ::_thesis: M is n -locally_euclidean now__::_thesis:_for_p_being_Point_of_M_ex_U_being_a_neighborhood_of_p_ex_S_being_open_Subset_of_(TOP-REAL_n)_st_U,S_are_homeomorphic let p be Point of M; ::_thesis: ex U being a_neighborhood of p ex S being open Subset of (TOP-REAL n) st U,S are_homeomorphic consider U being 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: the non empty ball Subset of (TOP-REAL n), [#] (TOP-REAL n) are_homeomorphic by Th10; reconsider S = the non empty ball Subset of (TOP-REAL n) as open Subset of (TOP-REAL n) ; take U = U; ::_thesis: ex S being open Subset of (TOP-REAL n) st U,S are_homeomorphic take S = S; ::_thesis: U,S are_homeomorphic A9: (TOP-REAL n) | ([#] (TOP-REAL n)) = TopStruct(# the carrier of (TOP-REAL n), the topology of (TOP-REAL n) #) by TSEP_1:93; A10: M | U, TopStruct(# the carrier of (TOP-REAL n), the topology 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: TopStruct(# the carrier of (TOP-REAL n), the topology 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; ::_thesis: verum end; hence M is n -locally_euclidean by Def4; ::_thesis: verum end; registration let n be Nat; cluster non empty TopSpace-like n -locally_euclidean -> non empty first-countable for TopStruct ; correctness coherence for b1 being non empty TopSpace st b1 is n -locally_euclidean holds b1 is first-countable ; proof let M be non empty TopSpace; ::_thesis: ( M is n -locally_euclidean implies M is first-countable ) assume A1: M is n -locally_euclidean ; ::_thesis: M is first-countable for p being Point of M ex B being Basis of p st B is countable proof let p be Point of M; ::_thesis: ex B being Basis of p st B is countable consider U being 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, TopStruct(# the carrier of (TOP-REAL n), the topology of (TOP-REAL n) #) are_homeomorphic by TSEP_1:93; then consider f being Function of (M | U),TopStruct(# the carrier of (TOP-REAL n), the topology of (TOP-REAL n) #) such that A3: f is being_homeomorphism by T_0TOPSP:def_1; A4: ( dom f = [#] (M | U) & rng f = [#] TopStruct(# the carrier of (TOP-REAL n), the topology 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_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 A8, 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; TOP-REAL n1 is first-countable ; then consider B1 being 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 H1( set ) -> Element of bool the carrier of M = ((f ") .: n) /\ (Int U); set B = { H1(X) where X is Element of A : X in B1 } ; A11: card B1 c= omega by A10, CARD_3:def_14; card { H1(X) where X is Element of A : X in B1 } c= card B1 from TREES_2:sch_2(); then A12: card { H1(X) where X is Element of A : X in B1 } c= omega by A11, XBOOLE_1:1; for x being set st x in { H1(X) where X is Element of A : X in B1 } holds x in bool the carrier of M proof let x be set ; ::_thesis: ( x in { H1(X) where X is Element of A : X in B1 } implies x in bool the carrier of M ) assume x in { H1(X) where X is Element of A : X in B1 } ; ::_thesis: x in bool the carrier of M then consider X1 being Element of A such that A13: ( x = H1(X1) & X1 in B1 ) ; thus x in bool the carrier of M by A13; ::_thesis: verum end; then reconsider B = { H1(X) where X is Element of A : X in B1 } as Subset-Family of M by TARSKI:def_3; A14: for P being Subset of M st P in B holds P is open proof let P be Subset of M; ::_thesis: ( P in B implies P is open ) assume P in B ; ::_thesis: P is open then consider X1 being Element of A such that A15: ( P = H1(X1) & X1 in B1 ) ; reconsider X1 = X1 as Subset of TopStruct(# the carrier of (TOP-REAL n), the topology of (TOP-REAL n) #) ; reconsider X2 = X1 as Subset of (TOP-REAL n) ; X2 is open by A15, YELLOW_8:12; then X2 in the topology of (TOP-REAL n) by PRE_TOPC:def_2; 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 TopStruct(# the carrier of (TOP-REAL n), the topology 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 being 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; ::_thesis: verum end; for Y being set st Y in B holds p in Y proof let Y be set ; ::_thesis: ( Y in B implies p in Y ) assume Y in B ; ::_thesis: p in Y then consider X1 being Element of A such that A21: ( Y = H1(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; ::_thesis: verum end; then A23: p in Intersect B by SETFAM_1:43; 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; ::_thesis: ( S is open & p in S implies ex V being Subset of M st ( V in B & V c= S ) ) assume A24: ( S is open & p in S ) ; ::_thesis: ex V being Subset of M st ( V in B & V c= S ) set S1 = S /\ ([#] (M | U)); S in the topology of M by A24, PRE_TOPC:def_2; then A25: S /\ ([#] (M | U)) in the topology of (M | U) by PRE_TOPC:def_4; reconsider U1 = M | U as non empty TopStruct by A8, A7; reconsider S1 = S /\ ([#] (M | U)) 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) ; f .: S1 in the topology of TopStruct(# the carrier of (TOP-REAL n), the topology of (TOP-REAL n) #) by A26, PRE_TOPC:def_2; then A27: S2 is open by 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 being Subset of (TOP-REAL n) such that A30: ( W in B1 & W c= S2 ) by A29, A27, YELLOW_8:13; reconsider W = W as Element of A ; set V = ((f ") .: W) /\ (Int U); reconsider V = ((f ") .: W) /\ (Int U) as Subset of M ; take V ; ::_thesis: ( V in B & V c= S ) thus V in B by A30; ::_thesis: V c= S 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; then (f ") .: W c= S by A32, A34, XBOOLE_1:1; hence V c= S by A33, XBOOLE_1:1; ::_thesis: verum end; then reconsider B = B as Basis of p by A14, A23, TOPS_2:def_1, YELLOW_8:def_1; take B ; ::_thesis: B is countable thus B is countable by A12, CARD_3:def_14; ::_thesis: verum end; hence M is first-countable by FRECHET:def_2; ::_thesis: verum end; end; set T = (TOP-REAL 0) | ([#] (TOP-REAL 0)); Lm2: (TOP-REAL 0) | ([#] (TOP-REAL 0)) = TopStruct(# the carrier of (TOP-REAL 0), the topology of (TOP-REAL 0) #) by TSEP_1:93; registration cluster non empty TopSpace-like 0 -locally_euclidean -> non empty discrete for TopStruct ; coherence for b1 being non empty TopSpace st b1 is 0 -locally_euclidean holds b1 is discrete proof let M be non empty TopSpace; ::_thesis: ( M is 0 -locally_euclidean implies M is discrete ) assume A1: M is 0 -locally_euclidean ; ::_thesis: M is discrete for X being Subset of M for p being Point of M st X = {p} holds X is open proof let X be Subset of M; ::_thesis: for p being Point of M st X = {p} holds X is open let p be Point of M; ::_thesis: ( X = {p} implies X is open ) assume A2: X = {p} ; ::_thesis: X is open consider U being 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; p in Int U by CONNSP_2:def_1; then A5: p in U by A4; M | U,(TOP-REAL 0) | ([#] (TOP-REAL 0)) are_homeomorphic by A3, METRIZTS:def_1; then consider f being Function of (M | U),((TOP-REAL 0) | ([#] (TOP-REAL 0))) such that A6: f is being_homeomorphism by T_0TOPSP:def_1; consider V being Subset of M such that A7: ( V is open & V c= U & p in V ) by CONNSP_2:6; for x being set holds ( x in V iff x = p ) proof let x be set ; ::_thesis: ( x in V iff x = p ) hereby ::_thesis: ( x = p implies x in V ) assume x in V ; ::_thesis: x = p 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, FUNCT_1:def_4; ::_thesis: verum end; assume x = p ; ::_thesis: x in V hence x in V by A7; ::_thesis: verum end; hence X is open by A2, A7, TARSKI:def_1; ::_thesis: verum end; hence M is discrete by TDLAT_3:17; ::_thesis: verum end; cluster non empty TopSpace-like discrete -> non empty 0 -locally_euclidean for TopStruct ; coherence for b1 being non empty TopSpace st b1 is discrete holds b1 is 0 -locally_euclidean proof A14: [#] ((TOP-REAL 0) | ([#] (TOP-REAL 0))) = {(0. (TOP-REAL 0))} by Lm2, EUCLID:22, EUCLID:77; let M be non empty TopSpace; ::_thesis: ( M is discrete implies M is 0 -locally_euclidean ) assume A15: M is discrete ; ::_thesis: M is 0 -locally_euclidean for p being Point of M ex U being a_neighborhood of p st U, [#] (TOP-REAL 0) are_homeomorphic proof let p be Point of M; ::_thesis: ex U being a_neighborhood of p st U, [#] (TOP-REAL 0) are_homeomorphic 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 = U as a_neighborhood of p by CONNSP_2:3; take U ; ::_thesis: U, [#] (TOP-REAL 0) are_homeomorphic set f = {[p,(0. (TOP-REAL 0))]}; A17: p in [#] (M | U) by A16, PRE_TOPC:def_5; A18: [p,(0. (TOP-REAL 0))] in [: the carrier of (M | U), the carrier of ((TOP-REAL 0) | ([#] (TOP-REAL 0))):] by A17, Lm2, ZFMISC_1:87; A19: dom {[p,(0. (TOP-REAL 0))]} = U by RELAT_1:9; then A20: dom {[p,(0. (TOP-REAL 0))]} = [#] (M | U) by PRE_TOPC:def_5; then reconsider f = {[p,(0. (TOP-REAL 0))]} as Function of (M | U),((TOP-REAL 0) | ([#] (TOP-REAL 0))) by A18, FUNCT_2:def_1, ZFMISC_1:31; A21: rng f = [#] ((TOP-REAL 0) | ([#] (TOP-REAL 0))) by A14, RELAT_1:9; for P being Subset of (M | U) holds ( P is closed iff f .: P is closed ) proof let P be Subset of (M | U); ::_thesis: ( P is closed iff f .: P is closed ) percases ( P is empty or not P is empty ) ; supposeA22: P is empty ; ::_thesis: ( P is closed iff f .: P is closed ) thus ( P is closed iff f .: P is closed ) by A22; ::_thesis: verum end; supposeA23: not P is empty ; ::_thesis: ( P is closed iff f .: P is closed ) 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; ::_thesis: ( f .: P is closed implies P is closed ) thus ( f .: P is closed implies P is closed ) by A23, A20, A19, ZFMISC_1:33; ::_thesis: verum end; end; end; then f is being_homeomorphism by A20, A21, TOPS_2:58; then M | U,(TOP-REAL 0) | ([#] (TOP-REAL 0)) are_homeomorphic by T_0TOPSP:def_1; hence U, [#] (TOP-REAL 0) are_homeomorphic by METRIZTS:def_1; ::_thesis: verum end; hence M is 0 -locally_euclidean by Th13; ::_thesis: verum end; end; registration let n be Nat; cluster TOP-REAL n -> second-countable ; correctness coherence TOP-REAL n is second-countable ; proof set T = TopStruct(# the carrier of (TOP-REAL n), the topology of (TOP-REAL n) #); A1: for x being set holds ( x in { (card B) where B is Basis of TopStruct(# the carrier of (TOP-REAL n), the topology of (TOP-REAL n) #) : verum } iff x in { (card B) where B is Basis of (TOP-REAL n) : verum } ) proof let x be set ; ::_thesis: ( x in { (card B) where B is Basis of TopStruct(# the carrier of (TOP-REAL n), the topology of (TOP-REAL n) #) : verum } iff x in { (card B) where B is Basis of (TOP-REAL n) : verum } ) hereby ::_thesis: ( x in { (card B) where B is Basis of (TOP-REAL n) : verum } implies x in { (card B) where B is Basis of TopStruct(# the carrier of (TOP-REAL n), the topology of (TOP-REAL n) #) : verum } ) assume x in { (card B) where B is Basis of TopStruct(# the carrier of (TOP-REAL n), the topology of (TOP-REAL n) #) : verum } ; ::_thesis: x in { (card B) where B is Basis of (TOP-REAL n) : verum } then consider B1 being Basis of TopStruct(# the carrier of (TOP-REAL n), the topology of (TOP-REAL n) #) 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) : verum } ; ::_thesis: verum end; assume x in { (card B) where B is Basis of (TOP-REAL n) : verum } ; ::_thesis: x in { (card B) where B is Basis of TopStruct(# the carrier of (TOP-REAL n), the topology of (TOP-REAL n) #) : verum } then consider B1 being Basis of (TOP-REAL n) such that A3: x = card B1 ; reconsider B2 = B1 as Basis of TopStruct(# the carrier of (TOP-REAL n), the topology of (TOP-REAL n) #) by YELLOW12:32; x = card B2 by A3; hence x in { (card B) where B is Basis of TopStruct(# the carrier of (TOP-REAL n), the topology of (TOP-REAL n) #) : verum } ; ::_thesis: verum end; weight TopStruct(# the carrier of (TOP-REAL n), the topology of (TOP-REAL n) #) = weight (TOP-REAL n) by A1, TARSKI:1; then weight (TOP-REAL n) c= omega by WAYBEL23:def_6; hence TOP-REAL n is second-countable by WAYBEL23:def_6; ::_thesis: verum end; end; registration let n be Nat; cluster non empty TopSpace-like Hausdorff second-countable n -locally_euclidean for TopStruct ; existence ex b1 being non empty TopSpace st ( b1 is second-countable & b1 is Hausdorff & b1 is n -locally_euclidean ) proof take TOP-REAL n ; ::_thesis: ( TOP-REAL n is second-countable & TOP-REAL n is Hausdorff & TOP-REAL n is n -locally_euclidean ) thus ( TOP-REAL n is second-countable & TOP-REAL n is Hausdorff & TOP-REAL n is n -locally_euclidean ) ; ::_thesis: verum end; end; definition let n be Nat; let M be non empty TopSpace; attrM is n -manifold means :Def5: :: MFOLD_1:def 5 ( M is second-countable & M is Hausdorff & M is n -locally_euclidean ); end; :: deftheorem Def5 defines -manifold MFOLD_1:def_5_:_ for n being Nat for M being non empty TopSpace holds ( M is n -manifold iff ( M is second-countable & M is Hausdorff & M is n -locally_euclidean ) ); definition let M be non empty TopSpace; attrM is manifold-like means :Def6: :: MFOLD_1:def 6 ex n being Nat st M is n -manifold ; end; :: deftheorem Def6 defines manifold-like MFOLD_1:def_6_:_ for M being non empty TopSpace holds ( M is manifold-like iff ex n being Nat st M is n -manifold ); registration let n be Nat; cluster non empty TopSpace-like n -manifold for TopStruct ; existence ex b1 being non empty TopSpace st b1 is n -manifold proof take TOP-REAL n ; ::_thesis: TOP-REAL n is n -manifold thus TOP-REAL n is n -manifold by Def5; ::_thesis: verum end; end; registration let n be Nat; cluster non empty TopSpace-like n -manifold -> non empty Hausdorff second-countable n -locally_euclidean for TopStruct ; correctness coherence for b1 being non empty TopSpace st b1 is n -manifold holds ( b1 is second-countable & b1 is Hausdorff & b1 is n -locally_euclidean ); by Def5; cluster non empty TopSpace-like Hausdorff second-countable n -locally_euclidean -> non empty n -manifold for TopStruct ; correctness coherence for b1 being non empty TopSpace st b1 is second-countable & b1 is Hausdorff & b1 is n -locally_euclidean holds b1 is n -manifold ; by Def5; cluster non empty TopSpace-like n -manifold -> non empty manifold-like for TopStruct ; correctness coherence for b1 being non empty TopSpace st b1 is n -manifold holds b1 is manifold-like ; by Def6; end; registration cluster non empty TopSpace-like second-countable discrete -> non empty 0 -manifold for TopStruct ; coherence for b1 being non empty TopSpace st b1 is second-countable & b1 is discrete holds b1 is 0 -manifold ; end; registration let n be Nat; let M be non empty n -manifold TopSpace; cluster non empty open -> non empty n -manifold for SubSpace of M; correctness coherence for b1 being non empty SubSpace of M st b1 is open holds b1 is n -manifold ; proof let X be non empty SubSpace of M; ::_thesis: ( X is open implies X is n -manifold ) assume A1: X is open ; ::_thesis: X is n -manifold [#] 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: TopStruct(# the carrier of X, the topology of X #) = TopStruct(# the carrier of (M | X1), the topology of (M | X1) #) by TSEP_1:5; A4: for x being set holds ( x in { (card B) where B is Basis of X : verum } iff x in { (card B) where B is Basis of (M | X1) : verum } ) proof let x be set ; ::_thesis: ( x in { (card B) where B is Basis of X : verum } iff x in { (card B) where B is Basis of (M | X1) : verum } ) hereby ::_thesis: ( x in { (card B) where B is Basis of (M | X1) : verum } implies x in { (card B) where B is Basis of X : verum } ) assume x in { (card B) where B is Basis of X : verum } ; ::_thesis: x in { (card B) where B is Basis of (M | X1) : verum } then consider B1 being 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) : verum } ; ::_thesis: verum end; assume x in { (card B) where B is Basis of (M | X1) : verum } ; ::_thesis: x in { (card B) where B is Basis of X : verum } then consider B1 being 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 : verum } ; ::_thesis: verum end; weight X = weight (M | X1) by A4, TARSKI:1; 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 ex U being a_neighborhood of p ex S being open Subset of (TOP-REAL n) st U,S are_homeomorphic proof let p be Point of X; ::_thesis: ex U being a_neighborhood of p ex S being open Subset of (TOP-REAL n) st U,S are_homeomorphic p in the carrier of X ; then reconsider p1 = p as Point of M by A2; consider U1 being a_neighborhood of p1, S1 being open Subset of (TOP-REAL n) such that A8: U1,S1 are_homeomorphic by Def4; consider U2 being open Subset of M, S2 being 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 non empty open 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 being 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 = 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) ; 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:18; 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_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 U3 is open by PRE_TOPC:def_2; then reconsider S = f .: U3 as open Subset of T2 by A14; S in the topology of T2 by PRE_TOPC:def_2; then consider Q being 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 = S as open Subset of (TOP-REAL n) by PRE_TOPC:def_2; take U ; ::_thesis: ex S being open Subset of (TOP-REAL n) st U,S are_homeomorphic take S ; ::_thesis: U,S are_homeomorphic 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: TopStruct(# the carrier of (X | U), the topology of (X | U) #) = TopStruct(# the carrier of ((M | U2) | U3), the topology 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; ::_thesis: verum end; then X is n -locally_euclidean by Def4; hence X is n -manifold by A7; ::_thesis: verum end; end; registration cluster non empty TopSpace-like manifold-like for TopStruct ; existence ex b1 being non empty TopSpace st b1 is manifold-like proof take TOP-REAL 0 ; ::_thesis: TOP-REAL 0 is manifold-like thus TOP-REAL 0 is manifold-like ; ::_thesis: verum end; end; definition mode manifold is non empty manifold-like TopSpace; end;