:: deftheorem defines BSPoly POLYALGX:def 6 :
for R being non degenerated comRing holds BSPoly R = (BSFSeri R) | ([#] (Polynom-Ring (1,R)));