let L be non empty unital doubleLoopStr ; :: thesis: 0_. L is with_roots
consider x being Element of L;
take x ; :: according to POLYNOM5:def 7 :: 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