let L be non empty unital doubleLoopStr ; :: thesis: 0_. L is with_roots
set x = the Element of L;
take the Element of L ; :: according to POLYNOM5:def 8 :: thesis: the Element of L is_a_root_of 0_. L
thus eval ((0_. L), the Element of L) = 0. L by POLYNOM4:17; :: according to POLYNOM5:def 7 :: thesis: verum