:: deftheorem defines Partial_Product CARDFIL3:def 7 :
for I being non empty set
for L being commutative TopGroup
for x being the carrier of b₂ -valued ManySortedSet of I
for b₄ being Function of ([#] (OrderedFIN I)), the carrier of L holds
( b₄ = Partial_Product x iff for j being Element of Fin I holds b₄ . j = Product (x,j) );