for X being RealNormSpace
for y1 being Point of X
for r being Real holds Ball (y1,r) = y1 + (Ball ((0. X),r))