theorem :: POLYNOM1:31

for n being Ordinal
for L being non empty non trivial right_complementable right_unital distributive Abelian add-associative right_zeroed associative doubleLoopStr holds 1. (Polynom-Ring (n,L)) = 1_ (n,L) by Def11;