theorem Th35: :: JORDAN1K:35
for q being Point of (TOP-REAL 2)
for r being Real
for x, y being Point of (Euclid 2) st y = |[0,0]| & x = q & r > 0 holds
(AffineMap (r,(q `1),r,(q `2))) .: (Ball (y,1)) = Ball (x,r)