:: deftheorem Def2 defines Formal-Series POLYALG1:def 2 :
for L being non empty doubleLoopStr
for b₂ being non empty strict AlgebraStr over L holds
( b₂ = Formal-Series L iff ( ( for x being set holds
( x in the carrier of b₂ iff x is sequence of L ) ) & ( for x, y being Element of b₂
for p, q being sequence of L st x = p & y = q holds
x + y = p + q ) & ( for x, y being Element of b₂
for p, q being sequence of L st x = p & y = q holds
x * y = p *' q ) & ( for a being Element of L
for x being Element of b₂
for p being sequence of L st x = p holds
a * x = a * p ) & 0. b₂ = 0_. L & 1. b₂ = 1_. L ) );