for n being Nat
for f being Function of (Tunit_ball n),(TOP-REAL n) st n <> 0 & ( for a being Point of (Tunit_ball n)
for b being Point of (TOP-REAL n) st a = b holds
f . a = (1 / (1 - (|.b.| * |.b.|))) * b ) holds
f is being_homeomorphism