theorem :: POLYNOM3:36

for L being non empty right_complementable Abelian add-associative right_zeroed well-unital distributive commutative doubleLoopStr holds 1. (Polynom-Ring L) = 1_. L by Def10;