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