theorem Th40: :: PREPOWER:40

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