theorem Th19: :: NAT_3:19

for X being set
for a, b being bag of X st support a misses support b holds
Product (a + b) = (Product a) * (Product b)