:: deftheorem Def3 defines Formal-Series POLYALGX:def 3 :
for n being Ordinal
for L being non degenerated comRing
for b₃ being non empty strict AlgebraStr over L holds
( b₃ = Formal-Series (n,L) iff ( ( for x being set holds
( x in the carrier of b₃ iff x is Series of n,L ) ) & ( for x, y being Element of b₃
for p, q being Series of n,L st x = p & y = q holds
x + y = p + q ) & ( for x, y being Element of b₃
for p, q being Series of n,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 Series of n,L st x = p holds
a * x = a * p ) & 0. b₃ = 0_ (n,L) & 1. b₃ = 1_ (n,L) ) );