let X be LinearTopSpace; :: thesis: for s being sequence of the carrier of X

for x being Point of X

for V being local_base of X

for B being Subset-Family of X st B = { (x + U) where U is Subset of X : ( U in V & U is a_neighborhood of 0. X ) } holds

( x in lim_f s iff for v being Element of B ex i being Nat st

for j being Nat st i <= j holds

s . j in v )

let s be sequence of the carrier of X; :: thesis: for x being Point of X

for V being local_base of X

for B being Subset-Family of X st B = { (x + U) where U is Subset of X : ( U in V & U is a_neighborhood of 0. X ) } holds

( x in lim_f s iff for v being Element of B ex i being Nat st

for j being Nat st i <= j holds

s . j in v )

let x be Point of X; :: thesis: for V being local_base of X

for B being Subset-Family of X st B = { (x + U) where U is Subset of X : ( U in V & U is a_neighborhood of 0. X ) } holds

( x in lim_f s iff for v being Element of B ex i being Nat st

for j being Nat st i <= j holds

s . j in v )

let V be local_base of X; :: thesis: for B being Subset-Family of X st B = { (x + U) where U is Subset of X : ( U in V & U is a_neighborhood of 0. X ) } holds

( x in lim_f s iff for v being Element of B ex i being Nat st

for j being Nat st i <= j holds

s . j in v )

let B be Subset-Family of X; :: thesis: ( B = { (x + U) where U is Subset of X : ( U in V & U is a_neighborhood of 0. X ) } implies ( x in lim_f s iff for v being Element of B ex i being Nat st

for j being Nat st i <= j holds

s . j in v ) )

assume B = { (x + U) where U is Subset of X : ( U in V & U is a_neighborhood of 0. X ) } ; :: thesis: ( x in lim_f s iff for v being Element of B ex i being Nat st

for j being Nat st i <= j holds

s . j in v )

then B is basis of (BOOL2F (NeighborhoodSystem x)) by Th10;

hence ( x in lim_f s iff for b being Element of B 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 X

for V being local_base of X

for B being Subset-Family of X st B = { (x + U) where U is Subset of X : ( U in V & U is a_neighborhood of 0. X ) } holds

( x in lim_f s iff for v being Element of B ex i being Nat st

for j being Nat st i <= j holds

s . j in v )

let s be sequence of the carrier of X; :: thesis: for x being Point of X

for V being local_base of X

for B being Subset-Family of X st B = { (x + U) where U is Subset of X : ( U in V & U is a_neighborhood of 0. X ) } holds

( x in lim_f s iff for v being Element of B ex i being Nat st

for j being Nat st i <= j holds

s . j in v )

let x be Point of X; :: thesis: for V being local_base of X

for B being Subset-Family of X st B = { (x + U) where U is Subset of X : ( U in V & U is a_neighborhood of 0. X ) } holds

( x in lim_f s iff for v being Element of B ex i being Nat st

for j being Nat st i <= j holds

s . j in v )

let V be local_base of X; :: thesis: for B being Subset-Family of X st B = { (x + U) where U is Subset of X : ( U in V & U is a_neighborhood of 0. X ) } holds

( x in lim_f s iff for v being Element of B ex i being Nat st

for j being Nat st i <= j holds

s . j in v )

let B be Subset-Family of X; :: thesis: ( B = { (x + U) where U is Subset of X : ( U in V & U is a_neighborhood of 0. X ) } implies ( x in lim_f s iff for v being Element of B ex i being Nat st

for j being Nat st i <= j holds

s . j in v ) )

assume B = { (x + U) where U is Subset of X : ( U in V & U is a_neighborhood of 0. X ) } ; :: thesis: ( x in lim_f s iff for v being Element of B ex i being Nat st

for j being Nat st i <= j holds

s . j in v )

then B is basis of (BOOL2F (NeighborhoodSystem x)) by Th10;

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

for j being Nat st i <= j holds

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