for L being non empty left_unital doubleLoopStr
for n being non zero Element of NAT holds
( (unital_poly (L,n)) . 0 = - (1_ L) & (unital_poly (L,n)) . n = 1_ L )