:: deftheorem defines rpoly HURWITZ:def 3 :
for L being non empty unital doubleLoopStr
for z being Element of L
for k being Element of NAT holds rpoly (k,z) = (0_. L) +* ((0,k) --> ((- ((power L) . (z,k))),(1_ L)));