theorem :: INT_8:13

for i, n being Nat
for fn being FinSequence of NAT st n > 1 & i,n are_coprime & len fn = order (i,n) & ( for d being Element of NAT st d in dom fn holds
fn . d = i |^ (d -' 1) ) holds
for d being Element of NAT st d in dom fn holds
((fn . d) |^ (order (i,n))) mod n = 1