:: deftheorem Def10 defines Polynom-Ring POLYNOM3:def 10 :
for L being non empty right_complementable add-associative right_zeroed distributive doubleLoopStr
for b₂ being non empty strict doubleLoopStr holds
( b₂ = Polynom-Ring L iff ( ( for x being set holds
( x in the carrier of b₂ iff x is Polynomial 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 ) & 0. b₂ = 0_. L & 1. b₂ = 1_. L ) );