theorem :: CLVECT_2:45

for X being ComplexUnitarySpace
for x, y being Point of X
for r being Real st y in Ball (x,r) holds
y - x in Ball ((0. X),r)