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