let I be set ; :: thesis: for G being TopaddGroup
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 TopaddGroup; :: 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