:: deftheorem Def4 defines BSFSeri POLYALGX:def 4 :
for R being non degenerated comRing
for b₂ being Function of (Formal-Series (1,R)),(Formal-Series R) holds
( b₂ = BSFSeri R iff for x being object st x in the carrier of (Formal-Series (1,R)) holds
ex x1 being Series of 1,R st
( x1 = x & b₂ . x = x1 * NBag1 ) );