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:15 ;
hence z is_a_root_of rpoly (1,z) by POLYNOM5:def 7; :: thesis: verum