let M be non empty locally_euclidean with_boundary TopSpace; :: thesis: for p being Point of M
for pM being Point of (M | (Fr M)) st p = pM holds
for U being a_neighborhood of p
for n being Nat
for h being Function of (M | U),(Tdisk ((0. (TOP-REAL n)),1)) st h is being_homeomorphism & h . p in Sphere ((0. (TOP-REAL n)),1) holds
ex n1 being Nat ex U being a_neighborhood of pM st
( n1 + 1 = n & (M | (Fr M)) | U, Tball ((0. (TOP-REAL n1)),1) are_homeomorphic )
let p be Point of M; :: thesis: for pM being Point of (M | (Fr M)) st p = pM holds
for U being a_neighborhood of p
for n being Nat
for h being Function of (M | U),(Tdisk ((0. (TOP-REAL n)),1)) st h is being_homeomorphism & h . p in Sphere ((0. (TOP-REAL n)),1) holds
ex n1 being Nat ex U being a_neighborhood of pM st
( n1 + 1 = n & (M | (Fr M)) | U, Tball ((0. (TOP-REAL n1)),1) are_homeomorphic )
let pM be Point of (M | (Fr M)); :: thesis: ( p = pM implies for U being a_neighborhood of p
for n being Nat
for h being Function of (M | U),(Tdisk ((0. (TOP-REAL n)),1)) st h is being_homeomorphism & h . p in Sphere ((0. (TOP-REAL n)),1) holds
ex n1 being Nat ex U being a_neighborhood of pM st
( n1 + 1 = n & (M | (Fr M)) | U, Tball ((0. (TOP-REAL n1)),1) are_homeomorphic ) )
assume A1: p = pM ; :: thesis: for U being a_neighborhood of p
for n being Nat
for h being Function of (M | U),(Tdisk ((0. (TOP-REAL n)),1)) st h is being_homeomorphism & h . p in Sphere ((0. (TOP-REAL n)),1) holds
ex n1 being Nat ex U being a_neighborhood of pM st
( n1 + 1 = n & (M | (Fr M)) | U, Tball ((0. (TOP-REAL n1)),1) are_homeomorphic )
let U be a_neighborhood of p; :: thesis: for n being Nat
for h being Function of (M | U),(Tdisk ((0. (TOP-REAL n)),1)) st h is being_homeomorphism & h . p in Sphere ((0. (TOP-REAL n)),1) holds
ex n1 being Nat ex U being a_neighborhood of pM st
( n1 + 1 = n & (M | (Fr M)) | U, Tball ((0. (TOP-REAL n1)),1) are_homeomorphic )
let n be Nat; :: thesis: for h being Function of (M | U),(Tdisk ((0. (TOP-REAL n)),1)) st h is being_homeomorphism & h . p in Sphere ((0. (TOP-REAL n)),1) holds
ex n1 being Nat ex U being a_neighborhood of pM st
( n1 + 1 = n & (M | (Fr M)) | U, Tball ((0. (TOP-REAL n1)),1) are_homeomorphic )
let h be Function of (M | U),(Tdisk ((0. (TOP-REAL n)),1)); :: thesis: ( h is being_homeomorphism & h . p in Sphere ((0. (TOP-REAL n)),1) implies ex n1 being Nat ex U being a_neighborhood of pM st
( n1 + 1 = n & (M | (Fr M)) | U, Tball ((0. (TOP-REAL n1)),1) are_homeomorphic ) )
assume that
A2: h is being_homeomorphism and
A3: h . p in Sphere ((0. (TOP-REAL n)),1) ; :: thesis: ex n1 being Nat ex U being a_neighborhood of pM st
( n1 + 1 = n & (M | (Fr M)) | U, Tball ((0. (TOP-REAL n1)),1) are_homeomorphic )
set TR = TOP-REAL n;
n > 0
proof
assume n <= 0 ; :: thesis: contradiction
then n = 0 ;
then h . p = 0. (TOP-REAL n) by A3, JORDAN2C:105;
then |.(0. (TOP-REAL n)).| = 1 by A3, TOPREAL9:12;
hence contradiction by EUCLID_2:42; :: thesis: verum
end;
then reconsider n1 = n - 1 as Element of NAT by NAT_1:20;
take n1 ; :: thesis: ex U being a_neighborhood of pM st
( n1 + 1 = n & (M | (Fr M)) | U, Tball ((0. (TOP-REAL n1)),1) are_homeomorphic )
M | U, Tdisk ((0. (TOP-REAL (n1 + 1))),1) are_homeomorphic by A2, T_0TOPSP:def 1;
then ex U being a_neighborhood of pM st (M | (Fr M)) | U, Tball ((0. (TOP-REAL n1)),1) are_homeomorphic by Th7, A1;
hence ex U being a_neighborhood of pM st
( n1 + 1 = n & (M | (Fr M)) | U, Tball ((0. (TOP-REAL n1)),1) are_homeomorphic ) ; :: thesis: verum