theorem :: EULER_2:16

for a, m being Nat
for F, G being integer-valued FinSequence holds (a * (F ^ G)) mod m = ((a * F) mod m) ^ ((a * G) mod m)