let z be non zero Nat; :: thesis: (2 |^ (2 |^ z)) mod 3 = 1
defpred S₁[ non zero Nat] means (2 |^ (2 |^ $1)) mod 3 = 1;
A1: S₁[1]

proof

2 |^ (2 |^ 1) = 2 * 2 by POLYEQ_5:1
.= (3 * 1) + 1 ;
hence S₁[1] by NAT_D:def 2; :: thesis: verum

end;

A2: for s being non zero Nat st S₁[s] holds
S₁[s + 1]

proof

let s be non zero Nat; :: thesis: ( S₁[s] implies S₁[s + 1] )
assume A3: S₁[s] ; :: thesis: S₁[s + 1]
2 |^ (s + 1) = (2 |^ s) * 2 by NEWTON:6;
then A4: 2 |^ (2 |^ (s + 1)) = (2 |^ (2 |^ s)) |^ 2 by NEWTON:9
.= (2 |^ (2 |^ s)) * (2 |^ (2 |^ s)) by POLYEQ_5:1 ;
((2 |^ (2 |^ s)) * (2 |^ (2 |^ s))) mod 3 = (1 * 1) mod 3 by A3, NAT_D:67;
hence S₁[s + 1] by A4, NAT_D:24; :: thesis: verum

end;

for s being non zero Nat holds S₁[s] from NAT_1:sch 10(A1, A2);
hence (2 |^ (2 |^ z)) mod 3 = 1 ; :: thesis: verum