theorem :: POLYALGX:22

for R being non degenerated comRing holds (0_ (1,R)) * NBag1 = 0_. R