let T be LinearTopSpace; :: thesis: for L being non empty reflexive transitive RelStr

for f being Function of ([#] L), the carrier of T

for x being Point of T

for V being local_base of T

for B being Subset-Family of T st [#] L is directed & B = { (x + U) where U is Subset of T : ( U in V & U is a_neighborhood of 0. T ) } holds

( x in lim_f f iff for b being Element of B ex i being Element of L st

for j being Element of L st i <= j holds

f . j in b )

let L be non empty reflexive transitive RelStr ; :: thesis: for f being Function of ([#] L), the carrier of T

for x being Point of T

for V being local_base of T

for B being Subset-Family of T st [#] L is directed & B = { (x + U) where U is Subset of T : ( U in V & U is a_neighborhood of 0. T ) } holds

( x in lim_f f iff for b being Element of B ex i being Element of L st

for j being Element of L st i <= j holds

f . j in b )

let f be Function of ([#] L), the carrier of T; :: thesis: for x being Point of T

for V being local_base of T

for B being Subset-Family of T st [#] L is directed & B = { (x + U) where U is Subset of T : ( U in V & U is a_neighborhood of 0. T ) } holds

( x in lim_f f iff for b being Element of B ex i being Element of L st

for j being Element of L st i <= j holds

f . j in b )

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

for B being Subset-Family of T st [#] L is directed & B = { (x + U) where U is Subset of T : ( U in V & U is a_neighborhood of 0. T ) } holds

( x in lim_f f iff for b being Element of B ex i being Element of L st

for j being Element of L st i <= j holds

f . j in b )

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

( x in lim_f f iff for b being Element of B ex i being Element of L st

for j being Element of L st i <= j holds

f . j in b )

let B be Subset-Family of T; :: thesis: ( [#] L is directed & B = { (x + U) where U is Subset of T : ( U in V & U is a_neighborhood of 0. T ) } implies ( x in lim_f f iff for b being Element of B ex i being Element of L st

for j being Element of L st i <= j holds

f . j in b ) )

assume that

A1: [#] L is directed and

A2: B = { (x + U) where U is Subset of T : ( U in V & U is a_neighborhood of 0. T ) } ; :: thesis: ( x in lim_f f iff for b being Element of B ex i being Element of L st

for j being Element of L st i <= j holds

f . j in b )

reconsider B1 = B as basis of (BOOL2F (NeighborhoodSystem x)) by A2, Th10;

( x in lim_f f iff for b being Element of B1 ex i being Element of L st

for j being Element of L st i <= j holds

f . j in b ) by A1, CARDFIL2:84;

hence ( x in lim_f f iff for b being Element of B ex i being Element of L st

for j being Element of L st i <= j holds

f . j in b ) ; :: thesis: verum

for f being Function of ([#] L), the carrier of T

for x being Point of T

for V being local_base of T

for B being Subset-Family of T st [#] L is directed & B = { (x + U) where U is Subset of T : ( U in V & U is a_neighborhood of 0. T ) } holds

( x in lim_f f iff for b being Element of B ex i being Element of L st

for j being Element of L st i <= j holds

f . j in b )

let L be non empty reflexive transitive RelStr ; :: thesis: for f being Function of ([#] L), the carrier of T

for x being Point of T

for V being local_base of T

for B being Subset-Family of T st [#] L is directed & B = { (x + U) where U is Subset of T : ( U in V & U is a_neighborhood of 0. T ) } holds

( x in lim_f f iff for b being Element of B ex i being Element of L st

for j being Element of L st i <= j holds

f . j in b )

let f be Function of ([#] L), the carrier of T; :: thesis: for x being Point of T

for V being local_base of T

for B being Subset-Family of T st [#] L is directed & B = { (x + U) where U is Subset of T : ( U in V & U is a_neighborhood of 0. T ) } holds

( x in lim_f f iff for b being Element of B ex i being Element of L st

for j being Element of L st i <= j holds

f . j in b )

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

for B being Subset-Family of T st [#] L is directed & B = { (x + U) where U is Subset of T : ( U in V & U is a_neighborhood of 0. T ) } holds

( x in lim_f f iff for b being Element of B ex i being Element of L st

for j being Element of L st i <= j holds

f . j in b )

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

( x in lim_f f iff for b being Element of B ex i being Element of L st

for j being Element of L st i <= j holds

f . j in b )

let B be Subset-Family of T; :: thesis: ( [#] L is directed & B = { (x + U) where U is Subset of T : ( U in V & U is a_neighborhood of 0. T ) } implies ( x in lim_f f iff for b being Element of B ex i being Element of L st

for j being Element of L st i <= j holds

f . j in b ) )

assume that

A1: [#] L is directed and

A2: B = { (x + U) where U is Subset of T : ( U in V & U is a_neighborhood of 0. T ) } ; :: thesis: ( x in lim_f f iff for b being Element of B ex i being Element of L st

for j being Element of L st i <= j holds

f . j in b )

reconsider B1 = B as basis of (BOOL2F (NeighborhoodSystem x)) by A2, Th10;

( x in lim_f f iff for b being Element of B1 ex i being Element of L st

for j being Element of L st i <= j holds

f . j in b ) by A1, CARDFIL2:84;

hence ( x in lim_f f iff for b being Element of B ex i being Element of L st

for j being Element of L st i <= j holds

f . j in b ) ; :: thesis: verum