theorem Th48: :: POLYALGX:48
for R being non degenerated comRing
for f, g being Element of (Polynom-Ring (1,R)) holds (BSPoly R) . (f + g) = ((BSPoly R) . f) + ((BSPoly R) . g)