let L be non empty unital doubleLoopStr ; :: thesis: for x being Element of L holds x is_a_root_of 0_. L
let x be Element of L; :: thesis: x is_a_root_of 0_. L
thus eval ((0_. L),x) = 0. L by POLYNOM4:17; :: according to POLYNOM5:def 6 :: thesis: verum