let M be non empty MetrSpace; 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); 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; ( 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
; 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 S1[ 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 & S1[n,O] )
consider f being Function such that
A4:
( dom f = NAT & rng f c= Balls x )
and
A5:
for n being object st n in NAT holds
S1[n,f . n]
from FUNCT_1:sch 6(A3);
reconsider f = f as sequence of (Balls x) by A4, FUNCT_2:2;
take
f
; for n being Element of NAT holds f . n = Ball (x9,(1 / (n + 1)))
let n be Element of NAT ; f . n = Ball (x9,(1 / (n + 1)))
S1[n,f . n]
by A5;
hence
f . n = Ball (x9,(1 / (n + 1)))
by A2, A1; verum