let n be natural number ; :: thesis: for B being non empty ball Subset of (TOP-REAL n) holds B, [#] (TOP-REAL n) are_homeomorphic
let B be non empty ball Subset of (TOP-REAL n); :: thesis: B, [#] (TOP-REAL n) are_homeomorphic
consider p being Point of (TOP-REAL n), r being real number such that
A1: B = Ball (p,r) by Def1;
reconsider B1 = Tball (p,r) as non empty TopSpace by A1;
A2: TOP-REAL n,(TOP-REAL n) | ([#] (TOP-REAL n)) are_homeomorphic by Th1;
A3: Tunit_ball n, TOP-REAL n are_homeomorphic by Th8;
r is positive by A1;
then Tball (p,r), Tball ((0. (TOP-REAL n)),1) are_homeomorphic by Th9;
then B1, TOP-REAL n are_homeomorphic by A3, BORSUK_3:3;
then Tball (p,r),(TOP-REAL n) | ([#] (TOP-REAL n)) are_homeomorphic by A2, BORSUK_3:3;
hence B, [#] (TOP-REAL n) are_homeomorphic by A1, METRIZTS:def 1; :: thesis: verum