theorem :: EULER_2:15

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