let M be non empty MetrSpace; :: thesis: for x being Point of
for x' being Point of st x = x' holds
ex f being Function of NAT , Balls x st
for n being Element of NAT holds f . n = Ball x',(1 / (n + 1))
let x be Point of ; :: thesis: for x' being Point of st x = x' holds
ex f being Function of NAT , Balls x st
for n being Element of NAT holds f . n = Ball x',(1 / (n + 1))
let x' be Point of ; :: thesis: ( x = x' implies ex f being Function of NAT , Balls x st
for n being Element of NAT holds f . n = Ball x',(1 / (n + 1)) )
assume A4: x = x' ; :: thesis: ex f being Function of NAT , Balls x st
for n being Element of NAT holds f . n = Ball x',(1 / (n + 1))
set B = Balls x;
consider x' being Point of such that
A0: ( x' = x & Balls x = { (Ball x',(1 / n)) where n is Element of NAT : n <> 0 } ) by Def10;
defpred S₁[ set , set ] means ex n' being Element of NAT st
( $1 = n' & $2 = Ball x',(1 / (n' + 1)) );
A12: for n being set st n in NAT holds
ex O being set st
( O in Balls x & S₁[n,O] )

proof

let n be set ; :: thesis: ( n in NAT implies ex O being set st
( O in Balls x & S₁[n,O] ) )
assume n in NAT ; :: thesis: ex O being set st
( O in Balls x & S₁[n,O] )
then reconsider n = n as Element of NAT ;
take Ball x',(1 / (n + 1)) ; :: thesis: ( Ball x',(1 / (n + 1)) in Balls x & S₁[n, Ball x',(1 / (n + 1))] )
thus ( Ball x',(1 / (n + 1)) in Balls x & S₁[n, Ball x',(1 / (n + 1))] ) by A0; :: thesis: verum

end;

consider f being Function such that
A13: ( dom f = NAT & rng f c= Balls x ) and
A14: for n being set st n in NAT holds
S₁[n,f . n] from WELLORD2:sch 1(A12);
reconsider f = f as Function of NAT , Balls x by A13, FUNCT_2:4;
take f ; :: thesis: for n being Element of NAT holds f . n = Ball x',(1 / (n + 1))
let n be Element of NAT ; :: thesis: f . n = Ball x',(1 / (n + 1))
S₁[n,f . n] by A14;
hence f . n = Ball x',(1 / (n + 1)) by A0, A4; :: thesis: verum