for L being non empty right_complementable add-associative right_zeroed well-unital distributive doubleLoopStr
for n being Element of NAT
for a being Element of L holds
( ( a <> 0. L implies len (monomial (a,n)) = n + 1 ) & ( a = 0. L implies len (monomial (a,n)) = 0 ) & len (monomial (a,n)) <= n + 1 )