theorem Th17: :: POLYALGX:17

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