let L be non empty non degenerated right_complementable well-unital Abelian add-associative right_zeroed doubleLoopStr ; :: thesis: for z being Element of L holds z is_a_root_of rpoly 1,z
let z be Element of L; :: thesis: z is_a_root_of rpoly 1,z
eval (rpoly 1,z),z = z - z by Th29
.= 0. L by RLVECT_1:28 ;
hence z is_a_root_of rpoly 1,z by POLYNOM5:def 6; :: thesis: verum