let a, b, c be Nat; :: thesis: (a |^ (2 * b)) mod c = (((a |^ b) mod c) * ((a |^ b) mod c)) mod c
reconsider a = a, b = b, c = c as Element of NAT by ORDINAL1:def 12;
(a |^ (2 * b)) mod c = (a |^ (b + b)) mod c
.= ((a |^ b) * (a |^ b)) mod c by NEWTON:8
.= (((a |^ b) mod c) * ((a |^ b) mod c)) mod c by NAT_D:67 ;
hence (a |^ (2 * b)) mod c = (((a |^ b) mod c) * ((a |^ b) mod c)) mod c ; :: thesis: verum