theorem :: POLYNOM3:37

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