:: deftheorem Def11 defines Polynom-Ring POLYNOM1:def 11 :
for n being Ordinal
for L being non trivial right_complementable right_unital distributive add-associative right_zeroed doubleLoopStr
for b₃ being non empty strict doubleLoopStr holds
( b₃ = Polynom-Ring (n,L) iff ( ( for x being set holds
( x in the carrier of b₃ iff x is Polynomial of n,L ) ) & ( for x, y being Element of b₃
for p, q being Polynomial of n,L st x = p & y = q holds
x + y = p + q ) & ( for x, y being Element of b₃
for p, q being Polynomial of n,L st x = p & y = q holds
x * y = p *' q ) & 0. b₃ = 0_ (n,L) & 1. b₃ = 1_ (n,L) ) );