theorem Th13: :: GROEB_2:13

for n being Ordinal
for L being non empty right_complementable add-associative right_zeroed addLoopStr
for p being Series of n,L
for b being bag of n holds b *' (- p) = - (b *' p)