:: deftheorem Def2 defines Product CARDFIL3:def 6 :
for I being non empty set
for L being commutative TopGroup
for x being the carrier of b₂ -valued ManySortedSet of I
for J being Element of Fin I
for b₅ being Element of L holds
( b₅ = Product (x,J) iff ex p being one-to-one FinSequence of I st
( rng p = J & b₅ = the multF of L "**" (# (p,x)) ) );