let k be Nat; :: thesis: 3 |^ (2 * k),1 are_congruent_mod 4
((2 * 4) + 1) mod 4 = 1 mod 4 by NAT_D:21
.= 1 by NAT_D:24 ;
then 3 |^ 2,1 are_congruent_mod 4 by Lm8;
then (3 |^ 2) |^ k,1 |^ k are_congruent_mod 4 by GR_CY_3:34;
hence 3 |^ (2 * k),1 are_congruent_mod 4 by NEWTON:9; :: thesis: verum