for I being non empty set
for G being commutative TopGroup
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_Product 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_Product s) . j in b ) by Th11;