theorem Th16: :: BROUWER3:17

for n being Nat
for p being Point of (TOP-REAL n)
for r, s being Real st s > 0 holds
( (mlt (s,(TOP-REAL n))) .: (Ball (p,r)) = Ball ((s * p),(r * s)) & (mlt (s,(TOP-REAL n))) .: (cl_Ball (p,r)) = cl_Ball ((s * p),(r * s)) & (mlt (s,(TOP-REAL n))) .: (Sphere (p,r)) = Sphere ((s * p),(r * s)) )