theorem Th22: :: TOPREAL9:24

for n being Nat
for a, b, r being Real
for x, y, z being Point of (TOP-REAL n) st a + b = 1 & |.a.| + |.b.| = 1 & b <> 0 & x in cl_Ball (z,r) & y in Ball (z,r) holds
(a * x) + (b * y) in Ball (z,r)