let n be Nat; :: thesis: 2 |^ (4 * n),1 are_congruent_mod 5
defpred S₁[ Nat] means 2 |^ (4 * $1),1 are_congruent_mod 5;
A1: S₁[ 0 ]

proof

2 |^ (4 * 0) = 1 by NEWTON:4;
hence 2 |^ (4 * 0),1 are_congruent_mod 5 by INT_1:11; :: thesis: verum

end;

A2: for k being Nat st S₁[k] holds
S₁[k + 1]

proof

let k be Nat; :: thesis: ( S₁[k] implies S₁[k + 1] )
assume A3: S₁[k] ; :: thesis: S₁[k + 1]
A4: 4 * (k + 1) = (4 * k) + (4 * 1) ;
5 * 3 = (2 |^ 4) - 1 by Lm4;
then 2 |^ (4 * 1),1 are_congruent_mod 5 ;
then (2 |^ (4 * k)) * (2 |^ (4 * 1)),1 * 1 are_congruent_mod 5 by A3, INT_1:18;
hence 2 |^ (4 * (k + 1)),1 are_congruent_mod 5 by A4, NEWTON:8; :: thesis: verum

end;

for k being Nat holds S₁[k] from NAT_1:sch 2(A1, A2);
hence 2 |^ (4 * n),1 are_congruent_mod 5 ; :: thesis: verum