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

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

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

then reconsider n1 = n - 1 as Element of NAT by NAT_1:20;
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 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

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