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:20; :: according to POLYNOM5:def 6 :: thesis: verum