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. ()),1)) st h is being_homeomorphism & h . p in Sphere ((0. ()),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. ()),1)) st h is being_homeomorphism & h . p in Sphere ((0. ()),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. ()),1)) st h is being_homeomorphism & h . p in Sphere ((0. ()),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. ()),1)) st h is being_homeomorphism & h . p in Sphere ((0. ()),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. ()),1)) st h is being_homeomorphism & h . p in Sphere ((0. ()),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. ()),1)) st h is being_homeomorphism & h . p in Sphere ((0. ()),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. ()),1)); :: thesis: ( h is being_homeomorphism & h . p in Sphere ((0. ()),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. ()),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. () by ;
then |.(0. ()).| = 1 by ;
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 ;
then ex U being a_neighborhood of pM st (M | (Fr M)) | U, Tball ((0. (TOP-REAL n1)),1) are_homeomorphic by ;
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