theorem Th16: :: POLYALGX:16

for n being Ordinal
for L being non degenerated comRing
for a being Element of L
for p, q being Series of n,L holds a * (p + q) = (a * p) + (a * q)