theorem Th2: :: NCFCONT1:2

for CNS being ComplexNormSpace
for x0 being Point of CNS
for g being Real st 0 < g holds
{ y where y is Point of CNS : ||.(y - x0).|| < g } is Neighbourhood of x0