theorem Th69: :: SRINGS_5:107

for r being Real
for n being non zero Nat
for p being Element of (EMINFTY n)
for t being object holds
( t in cl_Ball (p,r) iff ex f being Function st
( t = f & dom f = Seg n & ( for i being Nat st i in Seg n holds
f . i in [.(((@ p) . i) - r),(((@ p) . i) + r).] ) ) )