let k be Nat; :: thesis: 3 |^ (2 * k),1 are_congruent_mod 8
3 |^ 2,1 are_congruent_mod 8 by Lm8;
then (3 |^ 2) |^ k,1 |^ k are_congruent_mod 8 by GR_CY_3:34;
hence 3 |^ (2 * k),1 are_congruent_mod 8 by NEWTON:9; :: thesis: verum