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

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