for L being non empty non degenerated right_complementable well-unital Abelian add-associative right_zeroed doubleLoopStr
for z being Element of L holds z is_a_root_of rpoly (1,z)