let X be RealBanachSpace; for Y being SetSequence of X st union (rng Y) = the carrier of X & ( for n being Nat holds Y . n is closed ) holds
ex n0 being Nat ex r being Real ex x0 being Point of X st
( 0 < r & Ball (x0,r) c= Y . n0 )
let Y be SetSequence of X; ( union (rng Y) = the carrier of X & ( for n being Nat holds Y . n is closed ) implies ex n0 being Nat ex r being Real ex x0 being Point of X st
( 0 < r & Ball (x0,r) c= Y . n0 ) )
assume that
A1:
union (rng Y) = the carrier of X
and
A2:
for n being Nat holds Y . n is closed
; ex n0 being Nat ex r being Real ex x0 being Point of X st
( 0 < r & Ball (x0,r) c= Y . n0 )
then consider n0 being Nat, r being Real, xx0 being Point of (MetricSpaceNorm X) such that
A3:
( 0 < r & Ball (xx0,r) c= Y . n0 )
by A1, NORMSP_2:1;
consider x0 being Point of X such that
x0 = xx0
and
A4:
Ball (xx0,r) = { x where x is Point of X : ||.(x0 - x).|| < r }
by NORMSP_2:2;
Ball (x0,r) = { x where x is Point of X : ||.(x0 - x).|| < r }
;
hence
ex n0 being Nat ex r being Real ex x0 being Point of X st
( 0 < r & Ball (x0,r) c= Y . n0 )
by A3, A4; verum