theorem :: CARDFIL3:40

for I being non empty set
for G being Abelian TopaddGroup
for s being the carrier of b₂ -valued ManySortedSet of I
for x being Point of G
for B being basis of (BOOL2F (NeighborhoodSystem x)) holds
( x in lim_f (Partial_Sums s) 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
(Partial_Sums s) . j in b ) by Th12;