let n be Nat; :: 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 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 MFOLD_0:1;
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 MFOLD_0:3;
then B1, TOP-REAL n are_homeomorphic by A3, BORSUK_3:3;
hence B, [#] (TOP-REAL n) are_homeomorphic by A1, METRIZTS:def 1, A2, BORSUK_3:3; :: thesis: verum