theorem NDIFF824: :: LOPBAN11:13

for X being RealNormSpace-Sequence
for x being Point of (product X)
for r being Real st 0 < r holds
ex s being FinSequence of REAL ex Y being non-empty non empty FinSequence st
( dom s = dom X & dom Y = dom X & product Y c= Ball (x,r) & ( for i being Element of dom X holds
( 0 < s . i & s . i < r & Y . i = Ball ((x . i),(s . i)) ) ) )