theorem :: POLYNOM5:55

for L being non empty unital doubleLoopStr
for x being Element of L holds x is_a_root_of 0_. L by POLYNOM4:17;