let M be non empty MetrSpace; :: thesis: for s being sequence of the carrier of (TopSpaceMetr M)

for x being Point of (TopSpaceMetr M) holds

( x in lim_f s iff for b being Element of Balls x ex i being Nat st

for j being Nat st i <= j holds

s . j in b )

let s be sequence of the carrier of (TopSpaceMetr M); :: thesis: for x being Point of (TopSpaceMetr M) holds

( x in lim_f s iff for b being Element of Balls x ex i being Nat st

for j being Nat st i <= j holds

s . j in b )

let x be Point of (TopSpaceMetr M); :: thesis: ( x in lim_f s iff for b being Element of Balls x ex i being Nat st

for j being Nat st i <= j holds

s . j in b )

Balls x is basis of (BOOL2F (NeighborhoodSystem x)) by Th5;

hence ( x in lim_f s iff for b being Element of Balls x ex i being Nat st

for j being Nat st i <= j holds

s . j in b ) by CARDFIL2:97; :: thesis: verum

for x being Point of (TopSpaceMetr M) holds

( x in lim_f s iff for b being Element of Balls x ex i being Nat st

for j being Nat st i <= j holds

s . j in b )

let s be sequence of the carrier of (TopSpaceMetr M); :: thesis: for x being Point of (TopSpaceMetr M) holds

( x in lim_f s iff for b being Element of Balls x ex i being Nat st

for j being Nat st i <= j holds

s . j in b )

let x be Point of (TopSpaceMetr M); :: thesis: ( x in lim_f s iff for b being Element of Balls x ex i being Nat st

for j being Nat st i <= j holds

s . j in b )

Balls x is basis of (BOOL2F (NeighborhoodSystem x)) by Th5;

hence ( x in lim_f s iff for b being Element of Balls x ex i being Nat st

for j being Nat st i <= j holds

s . j in b ) by CARDFIL2:97; :: thesis: verum