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