theorem Th7: :: MFOLD_1:7

for n being Nat
for p being Point of (TOP-REAL n)
for r being positive Real
for f being Function of (Tunit_ball n),(Tball (p,r)) 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 = (r * b) + p ) holds
f is being_homeomorphism