theorem Th9: :: EUCLID_9:9

for n being Nat
for r being Real
for a, o, p being Element of (TOP-REAL n) st a in Ball (o,r) holds
for x being object holds
( |.((a - o) . x).| < r & |.((a . x) - (o . x)).| < r )