let I be set ; :: thesis: for G being TopGroup

for f being Function of ([#] (OrderedFIN I)), the carrier of G

for x being Point of G

for B being basis of (BOOL2F (NeighborhoodSystem x)) holds

( x in lim_f f iff for b being Element of B ex i being Element of (OrderedFIN I) st

for j being Element of (OrderedFIN I) st i <= j holds

f . j in b )

let G be TopGroup; :: thesis: for f being Function of ([#] (OrderedFIN I)), the carrier of G

for x being Point of G

for B being basis of (BOOL2F (NeighborhoodSystem x)) holds

( x in lim_f f iff for b being Element of B ex i being Element of (OrderedFIN I) st

for j being Element of (OrderedFIN I) st i <= j holds

f . j in b )

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

for B being basis of (BOOL2F (NeighborhoodSystem x)) holds

( x in lim_f f iff for b being Element of B ex i being Element of (OrderedFIN I) st

for j being Element of (OrderedFIN I) st i <= j holds

f . j in b )

let x be Point of G; :: thesis: for B being basis of (BOOL2F (NeighborhoodSystem x)) holds

( x in lim_f f iff for b being Element of B ex i being Element of (OrderedFIN I) st

for j being Element of (OrderedFIN I) st i <= j holds

f . j in b )

let B be basis of (BOOL2F (NeighborhoodSystem x)); :: thesis: ( x in lim_f f iff for b being Element of B ex i being Element of (OrderedFIN I) st

for j being Element of (OrderedFIN I) st i <= j holds

f . j in b )

[#] (OrderedFIN I) is directed by Th4;

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

for j being Element of (OrderedFIN I) st i <= j holds

f . j in b ) by CARDFIL2:84; :: thesis: verum

for f being Function of ([#] (OrderedFIN I)), the carrier of G

for x being Point of G

for B being basis of (BOOL2F (NeighborhoodSystem x)) holds

( x in lim_f f iff for b being Element of B ex i being Element of (OrderedFIN I) st

for j being Element of (OrderedFIN I) st i <= j holds

f . j in b )

let G be TopGroup; :: thesis: for f being Function of ([#] (OrderedFIN I)), the carrier of G

for x being Point of G

for B being basis of (BOOL2F (NeighborhoodSystem x)) holds

( x in lim_f f iff for b being Element of B ex i being Element of (OrderedFIN I) st

for j being Element of (OrderedFIN I) st i <= j holds

f . j in b )

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

for B being basis of (BOOL2F (NeighborhoodSystem x)) holds

( x in lim_f f iff for b being Element of B ex i being Element of (OrderedFIN I) st

for j being Element of (OrderedFIN I) st i <= j holds

f . j in b )

let x be Point of G; :: thesis: for B being basis of (BOOL2F (NeighborhoodSystem x)) holds

( x in lim_f f iff for b being Element of B ex i being Element of (OrderedFIN I) st

for j being Element of (OrderedFIN I) st i <= j holds

f . j in b )

let B be basis of (BOOL2F (NeighborhoodSystem x)); :: thesis: ( x in lim_f f iff for b being Element of B ex i being Element of (OrderedFIN I) st

for j being Element of (OrderedFIN I) st i <= j holds

f . j in b )

[#] (OrderedFIN I) is directed by Th4;

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

for j being Element of (OrderedFIN I) st i <= j holds

f . j in b ) by CARDFIL2:84; :: thesis: verum