for a, m, i being Nat
for A being sequence of NAT st A . 0 = a mod m & ( for j being Nat holds A . (j + 1) = ((A . j) * (A . j)) mod m ) holds
A . i = (a to_power (2 to_power i)) mod m