theorem Th23: :: POLYALGX:23

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