theorem :: TOPREALC:26

for n being Nat
for r being Real
for a, o being Point of (TOP-REAL n) st n <> 0 & a in Ball (o,r) holds
|.(Sum (a - o)).| < n * r