theorem Th44: :: NUMBER19:44

for L being non empty right_complementable add-associative right_zeroed distributive unital doubleLoopStr
for z being Element of the carrier of L
for k being Element of NAT holds rpoly (<*k*>,<*z*>) = <*(rpoly (k,z))*>