theorem Th12: :: GROEB_2:12

for n being Ordinal
for L being non empty right-distributive right_zeroed doubleLoopStr
for p, q being Series of n,L
for b being bag of n holds b *' (p + q) = (b *' p) + (b *' q)