let n be odd Nat; :: thesis:
consider m being Nat such that
L0: n = (2 * m) + 1 by ABIAN:9;
defpred S₁[ Nat] means (2 |^ ((2 * $1) + 1)) mod 3 = 2;
L1: S₁[ 0 ] by NAT_D:63;
L2: for k being Nat st S₁[k] holds
S₁[k + 1]

let k be Nat; :: thesis:
assume A1: S₁[k] ; :: thesis:
A2: 1 = 1 mod 3 by NAT_D:63
.= ((1 * 3) + 1) mod 3 by NAT_D:21
.= (2 * 2) mod 3
.= (2 |^ 2) mod 3 by NEWTON:81 ;
2 = (2 * 1) mod 3 by NAT_D:63
.= ((2 |^ ((2 * k) + 1)) * (2 |^ 2)) mod 3 by A1, A2, NAT_D:67
.= (2 |^ (((2 * k) + 1) + 2)) mod 3 by NEWTON:8
.= (2 |^ ((2 * (k + 1)) + 1)) mod 3 ;
hence S₁[k + 1] ; :: thesis:

end;