for L being non empty unital doubleLoopStr
for z being Element of L
for k being Element of NAT st k <> 0 holds
( (rpoly (k,z)) . 0 = - ((power L) . (z,k)) & (rpoly (k,z)) . k = 1_ L ) by Lm10;