theorem Th16: :: NUMBER08:16

for X being set
for b1, b2 being complex-valued finite-support ManySortedSet of X st support b1 = support b2 holds
Product (b1 (#) b2) = (Product b1) * (Product b2)