set M = TUnitSphere n;
for p being Point of () ex U being a_neighborhood of p st U, [#] () are_homeomorphic
proof
let p be Point of (); :: thesis: ex U being a_neighborhood of p st U, [#] () 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 ;
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 () by TOPREALB:def 7;
then reconsider A = {(- p1)} as Subset of () by ZFMISC_1:31;
reconsider U1 = ([#] ()) \ A as Subset of () ;
|.(0. (TOP-REAL n1)).| <> |.(- p1).| by ;
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 ;
take U ; :: thesis:
reconsider m = n + 1 as Nat ;
A5: TUnitSphere n = Tcircle ((0. ()),1) by TOPREALB:def 7
.= () | (Sphere ((0. ()),1)) by TOPREALB:def 6 ;
reconsider S = Sphere ((0. ()),1) as Subset of () ;
reconsider U11 = U1 as Subset of (() | S) by A5;
U1 c= [#] () ;
then A6: U1 c= Sphere ((0. ()),1) by ;
then reconsider V = U11 as non empty Subset of () by ;
(TUnitSphere n) | U = () | V by ;
then reconsider U2 = () | U as non empty SubSpace of TOP-REAL m ;
reconsider p2 = - p1 as Point of () ;
p2 <> 0. () by ;
then A7: TOP-REAL n, TPlane (p2,(0. ())) are_homeomorphic by Th29;
A8: (TOP-REAL n) | ([#] ()) = TopStruct(# the carrier of (), the topology of () #) by TSEP_1:93;
A9: TOP-REAL n, TopStruct(# the carrier of (), the topology of () #) are_homeomorphic by YELLOW14:19;
[#] U2 = U by PRE_TOPC:def 5
.= the carrier of (Tcircle ((0. ()),1)) \ {p2} by TOPREALB:def 7
.= ([#] (() | (Sphere ((0. ()),1)))) \ {p2} by TOPREALB:def 6
.= (Sphere ((0. ()),1)) \ {p2} by PRE_TOPC:def 5 ;
then stereographic_projection (U2,p2) is being_homeomorphism by ;
then U2, TPlane (p2,(0. ())) are_homeomorphic by T_0TOPSP:def 1;
then TOP-REAL n,U2 are_homeomorphic by ;
hence U, [#] () are_homeomorphic by ; :: thesis: verum
end;
hence ( TUnitSphere n is without_boundary & TUnitSphere n is n -locally_euclidean ) by MFOLD_1:14; :: thesis: verum