theorem Th49: :: POLYALGX:49
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)