for L being non empty unital doubleLoopStr
for z being Element of L
for i, k being Element of NAT st i <> 0 & i <> k holds
(rpoly (k,z)) . i = 0. L by Lm11;