theorem :: POLYALGX:36

for R being non degenerated comRing
for f1, g1 being sequence of R holds (f1 + g1) * BagN1 = (f1 * BagN1) + (g1 * BagN1)