let M be non empty MetrSpace; :: thesis: for x being Point of (TopSpaceMetr M)

for x9 being Point of M st x = x9 holds

ex f being sequence of (Balls x) st

for n being Element of NAT holds f . n = Ball (x9,(1 / (n + 1)))

let x be Point of (TopSpaceMetr M); :: thesis: for x9 being Point of M st x = x9 holds

ex f being sequence of (Balls x) st

for n being Element of NAT holds f . n = Ball (x9,(1 / (n + 1)))

let x9 be Point of M; :: thesis: ( x = x9 implies ex f being sequence of (Balls x) st

for n being Element of NAT holds f . n = Ball (x9,(1 / (n + 1))) )

assume A1: x = x9 ; :: thesis: ex f being sequence of (Balls x) st

for n being Element of NAT holds f . n = Ball (x9,(1 / (n + 1)))

set B = Balls x;

consider x9 being Point of M such that

A2: ( x9 = x & Balls x = { (Ball (x9,(1 / n))) where n is Nat : n <> 0 } ) by Def1;

defpred S_{1}[ object , object ] means ex n9 being Element of NAT st

( $1 = n9 & $2 = Ball (x9,(1 / (n9 + 1))) );

A3: for n being object st n in NAT holds

ex O being object st

( O in Balls x & S_{1}[n,O] )

A4: ( dom f = NAT & rng f c= Balls x ) and

A5: for n being object st n in NAT holds

S_{1}[n,f . n]
from FUNCT_1:sch 6(A3);

reconsider f = f as sequence of (Balls x) by A4, FUNCT_2:2;

take f ; :: thesis: for n being Element of NAT holds f . n = Ball (x9,(1 / (n + 1)))

let n be Element of NAT ; :: thesis: f . n = Ball (x9,(1 / (n + 1)))

S_{1}[n,f . n]
by A5;

hence f . n = Ball (x9,(1 / (n + 1))) by A2, A1; :: thesis: verum

for x9 being Point of M st x = x9 holds

ex f being sequence of (Balls x) st

for n being Element of NAT holds f . n = Ball (x9,(1 / (n + 1)))

let x be Point of (TopSpaceMetr M); :: thesis: for x9 being Point of M st x = x9 holds

ex f being sequence of (Balls x) st

for n being Element of NAT holds f . n = Ball (x9,(1 / (n + 1)))

let x9 be Point of M; :: thesis: ( x = x9 implies ex f being sequence of (Balls x) st

for n being Element of NAT holds f . n = Ball (x9,(1 / (n + 1))) )

assume A1: x = x9 ; :: thesis: ex f being sequence of (Balls x) st

for n being Element of NAT holds f . n = Ball (x9,(1 / (n + 1)))

set B = Balls x;

consider x9 being Point of M such that

A2: ( x9 = x & Balls x = { (Ball (x9,(1 / n))) where n is Nat : n <> 0 } ) by Def1;

defpred S

( $1 = n9 & $2 = Ball (x9,(1 / (n9 + 1))) );

A3: for n being object st n in NAT holds

ex O being object st

( O in Balls x & S

proof

consider f being Function such that
let n be object ; :: thesis: ( n in NAT implies ex O being object st

( O in Balls x & S_{1}[n,O] ) )

assume n in NAT ; :: thesis: ex O being object st

( O in Balls x & S_{1}[n,O] )

then reconsider n = n as Element of NAT ;

take Ball (x9,(1 / (n + 1))) ; :: thesis: ( Ball (x9,(1 / (n + 1))) in Balls x & S_{1}[n, Ball (x9,(1 / (n + 1)))] )

thus ( Ball (x9,(1 / (n + 1))) in Balls x & S_{1}[n, Ball (x9,(1 / (n + 1)))] )
by A2; :: thesis: verum

end;( O in Balls x & S

assume n in NAT ; :: thesis: ex O being object st

( O in Balls x & S

then reconsider n = n as Element of NAT ;

take Ball (x9,(1 / (n + 1))) ; :: thesis: ( Ball (x9,(1 / (n + 1))) in Balls x & S

thus ( Ball (x9,(1 / (n + 1))) in Balls x & S

A4: ( dom f = NAT & rng f c= Balls x ) and

A5: for n being object st n in NAT holds

S

reconsider f = f as sequence of (Balls x) by A4, FUNCT_2:2;

take f ; :: thesis: for n being Element of NAT holds f . n = Ball (x9,(1 / (n + 1)))

let n be Element of NAT ; :: thesis: f . n = Ball (x9,(1 / (n + 1)))

S

hence f . n = Ball (x9,(1 / (n + 1))) by A2, A1; :: thesis: verum