theorem Th45: :: PREPOWER:45

for a being Real
for k, l being Integer holds (a #Z k) #Z l = a #Z (k * l)