let a be Nat; :: thesis: for b, n being non zero Nat st a mod b = 1 holds
(a |^ n) mod b = 1
let b, n be non zero Nat; :: thesis: ( a mod b = 1 implies (a |^ n) mod b = 1 )
assume a mod b = 1 ; :: thesis: (a |^ n) mod b = 1
then 1 = ((a mod b) |^ n) mod b ;
hence (a |^ n) mod b = 1 by GR_CY_3:30; :: thesis: verum