theorem :: CARDFIL3:36

for I being non empty set
for L being commutative TopGroup
for x being the carrier of b₂ -valued ManySortedSet of I
for J, e being Element of Fin I st e = {} holds
( Product (x,e) = 1_ L & ( for e, f being Element of Fin I st e misses f holds
Product (x,(e \/ f)) = (Product (x,e)) * (Product (x,f)) ) )