set M = TUnitSphere n;

for p being Point of (TUnitSphere n) ex U being a_neighborhood of p st U, [#] (TOP-REAL n) are_homeomorphic

for p being Point of (TUnitSphere n) ex U being a_neighborhood of p st U, [#] (TOP-REAL n) are_homeomorphic

proof

hence
( TUnitSphere n is without_boundary & TUnitSphere n is n -locally_euclidean )
by MFOLD_1:14; :: thesis: verum
let p be Point of (TUnitSphere n); :: thesis: ex U being a_neighborhood of p st U, [#] (TOP-REAL n) are_homeomorphic

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

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

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

A1: |.p1.| = 1 by TOPREALB:12;

A2: |.(- p1).| = sqrt |((- p1),(- p1))| by EUCLID_2:37

.= sqrt |(p1,p1)| by EUCLID_2:23

.= 1 by A1, EUCLID_2:37 ;

then |.((- p1) + (0. (TOP-REAL n1))).| = 1 by RLVECT_1:4;

then |.((- p1) + ((- 1) * (0. (TOP-REAL n1)))).| = 1 by RLVECT_1:10;

then B3: |.((- p1) - (0. (TOP-REAL n1))).| = 1 by RLVECT_1:16;

then - p1 in Sphere ((0. (TOP-REAL n1)),1) by TOPREAL9:9;

then - p1 in [#] ((TOP-REAL n1) | (Sphere ((0. (TOP-REAL n1)),1))) by PRE_TOPC:def 5;

then - p1 in the carrier of (Tcircle ((0. (TOP-REAL n1)),1)) by TOPREALB:def 6;

then - p1 in the carrier of (Tunit_circle n1) by TOPREALB:def 7;

then reconsider A = {(- p1)} as Subset of (TUnitSphere n) by ZFMISC_1:31;

reconsider U1 = ([#] (TUnitSphere n)) \ A as Subset of (TUnitSphere n) ;

|.(0. (TOP-REAL n1)).| <> |.(- p1).| by A2, EUCLID_2:39;

then 0. (TOP-REAL n1) <> (1 + 1) * (- p1) by RLVECT_1:11;

then 0. (TOP-REAL n1) <> (1 * (- p1)) + (1 * (- p1)) by RLVECT_1:def 6;

then 0. (TOP-REAL n1) <> (1 * (- p1)) + (- p1) by RLVECT_1:def 8;

then 0. (TOP-REAL n1) <> (- p1) + (- p1) by RLVECT_1:def 8;

then (- p1) + (- (- p1)) <> (- p1) + (- p1) by RLVECT_1:5;

then A4: not p1 in {(- p1)} by TARSKI:def 1;

then p1 in U1 by XBOOLE_0:def 5;

then reconsider U = U1 as a_neighborhood of p by CONNSP_2:3, FRECHET:4;

take U ; :: thesis: U, [#] (TOP-REAL n) are_homeomorphic

reconsider m = n + 1 as Nat ;

A5: TUnitSphere n = Tcircle ((0. (TOP-REAL m)),1) by TOPREALB:def 7

.= (TOP-REAL m) | (Sphere ((0. (TOP-REAL m)),1)) by TOPREALB:def 6 ;

reconsider S = Sphere ((0. (TOP-REAL m)),1) as Subset of (TOP-REAL m) ;

reconsider U11 = U1 as Subset of ((TOP-REAL m) | S) by A5;

U1 c= [#] (Tunit_circle m) ;

then A6: U1 c= Sphere ((0. (TOP-REAL m)),1) by A5, PRE_TOPC:def 5;

then reconsider V = U11 as non empty Subset of (TOP-REAL m) by A4, XBOOLE_0:def 5, XBOOLE_1:1;

(TUnitSphere n) | U = (TOP-REAL m) | V by A5, A6, PRE_TOPC:7;

then reconsider U2 = (TUnitSphere n) | U as non empty SubSpace of TOP-REAL m ;

reconsider p2 = - p1 as Point of (TOP-REAL m) ;

p2 <> 0. (TOP-REAL m) by A2, EUCLID_2:39;

then A7: TOP-REAL n, TPlane (p2,(0. (TOP-REAL m))) are_homeomorphic by Th29;

A8: (TOP-REAL n) | ([#] (TOP-REAL n)) = TopStruct(# the carrier of (TOP-REAL n), the topology of (TOP-REAL n) #) by TSEP_1:93;

A9: TOP-REAL n, TopStruct(# the carrier of (TOP-REAL n), the topology of (TOP-REAL n) #) are_homeomorphic by YELLOW14:19;

[#] U2 = U by PRE_TOPC:def 5

.= the carrier of (Tcircle ((0. (TOP-REAL m)),1)) \ {p2} by TOPREALB:def 7

.= ([#] ((TOP-REAL m) | (Sphere ((0. (TOP-REAL m)),1)))) \ {p2} by TOPREALB:def 6

.= (Sphere ((0. (TOP-REAL m)),1)) \ {p2} by PRE_TOPC:def 5 ;

then stereographic_projection (U2,p2) is being_homeomorphism by B3, TOPREAL9:9, Th31;

then U2, TPlane (p2,(0. (TOP-REAL m))) are_homeomorphic by T_0TOPSP:def 1;

then TOP-REAL n,U2 are_homeomorphic by A7, BORSUK_3:3;

hence U, [#] (TOP-REAL n) are_homeomorphic by A8, METRIZTS:def 1, A9, BORSUK_3:3; :: thesis: verum

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

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

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

A1: |.p1.| = 1 by TOPREALB:12;

A2: |.(- p1).| = sqrt |((- p1),(- p1))| by EUCLID_2:37

.= sqrt |(p1,p1)| by EUCLID_2:23

.= 1 by A1, EUCLID_2:37 ;

then |.((- p1) + (0. (TOP-REAL n1))).| = 1 by RLVECT_1:4;

then |.((- p1) + ((- 1) * (0. (TOP-REAL n1)))).| = 1 by RLVECT_1:10;

then B3: |.((- p1) - (0. (TOP-REAL n1))).| = 1 by RLVECT_1:16;

then - p1 in Sphere ((0. (TOP-REAL n1)),1) by TOPREAL9:9;

then - p1 in [#] ((TOP-REAL n1) | (Sphere ((0. (TOP-REAL n1)),1))) by PRE_TOPC:def 5;

then - p1 in the carrier of (Tcircle ((0. (TOP-REAL n1)),1)) by TOPREALB:def 6;

then - p1 in the carrier of (Tunit_circle n1) by TOPREALB:def 7;

then reconsider A = {(- p1)} as Subset of (TUnitSphere n) by ZFMISC_1:31;

reconsider U1 = ([#] (TUnitSphere n)) \ A as Subset of (TUnitSphere n) ;

|.(0. (TOP-REAL n1)).| <> |.(- p1).| by A2, EUCLID_2:39;

then 0. (TOP-REAL n1) <> (1 + 1) * (- p1) by RLVECT_1:11;

then 0. (TOP-REAL n1) <> (1 * (- p1)) + (1 * (- p1)) by RLVECT_1:def 6;

then 0. (TOP-REAL n1) <> (1 * (- p1)) + (- p1) by RLVECT_1:def 8;

then 0. (TOP-REAL n1) <> (- p1) + (- p1) by RLVECT_1:def 8;

then (- p1) + (- (- p1)) <> (- p1) + (- p1) by RLVECT_1:5;

then A4: not p1 in {(- p1)} by TARSKI:def 1;

then p1 in U1 by XBOOLE_0:def 5;

then reconsider U = U1 as a_neighborhood of p by CONNSP_2:3, FRECHET:4;

take U ; :: thesis: U, [#] (TOP-REAL n) are_homeomorphic

reconsider m = n + 1 as Nat ;

A5: TUnitSphere n = Tcircle ((0. (TOP-REAL m)),1) by TOPREALB:def 7

.= (TOP-REAL m) | (Sphere ((0. (TOP-REAL m)),1)) by TOPREALB:def 6 ;

reconsider S = Sphere ((0. (TOP-REAL m)),1) as Subset of (TOP-REAL m) ;

reconsider U11 = U1 as Subset of ((TOP-REAL m) | S) by A5;

U1 c= [#] (Tunit_circle m) ;

then A6: U1 c= Sphere ((0. (TOP-REAL m)),1) by A5, PRE_TOPC:def 5;

then reconsider V = U11 as non empty Subset of (TOP-REAL m) by A4, XBOOLE_0:def 5, XBOOLE_1:1;

(TUnitSphere n) | U = (TOP-REAL m) | V by A5, A6, PRE_TOPC:7;

then reconsider U2 = (TUnitSphere n) | U as non empty SubSpace of TOP-REAL m ;

reconsider p2 = - p1 as Point of (TOP-REAL m) ;

p2 <> 0. (TOP-REAL m) by A2, EUCLID_2:39;

then A7: TOP-REAL n, TPlane (p2,(0. (TOP-REAL m))) are_homeomorphic by Th29;

A8: (TOP-REAL n) | ([#] (TOP-REAL n)) = TopStruct(# the carrier of (TOP-REAL n), the topology of (TOP-REAL n) #) by TSEP_1:93;

A9: TOP-REAL n, TopStruct(# the carrier of (TOP-REAL n), the topology of (TOP-REAL n) #) are_homeomorphic by YELLOW14:19;

[#] U2 = U by PRE_TOPC:def 5

.= the carrier of (Tcircle ((0. (TOP-REAL m)),1)) \ {p2} by TOPREALB:def 7

.= ([#] ((TOP-REAL m) | (Sphere ((0. (TOP-REAL m)),1)))) \ {p2} by TOPREALB:def 6

.= (Sphere ((0. (TOP-REAL m)),1)) \ {p2} by PRE_TOPC:def 5 ;

then stereographic_projection (U2,p2) is being_homeomorphism by B3, TOPREAL9:9, Th31;

then U2, TPlane (p2,(0. (TOP-REAL m))) are_homeomorphic by T_0TOPSP:def 1;

then TOP-REAL n,U2 are_homeomorphic by A7, BORSUK_3:3;

hence U, [#] (TOP-REAL n) are_homeomorphic by A8, METRIZTS:def 1, A9, BORSUK_3:3; :: thesis: verum