:: deftheorem Def6 defines Polynom-Algebra POLYALG1:def 6 :
for L being non empty right_complementable distributive add-associative right_zeroed doubleLoopStr
for b₂ being non empty strict AlgebraStr over L holds
( b₂ = Polynom-Algebra L iff ex A being non empty Subset of (Formal-Series L) st
( A = the carrier of (Polynom-Ring L) & b₂ = GenAlg A ) );