let a be non trivial Nat; :: thesis: for i, j being Integer holds (sgn ((4 * i) + j)) * (Py (a,|.((4 * i) + j).|)),(sgn j) * (Py (a,|.j.|)) are_congruent_mod Px (a,|.i.|)
let i, j be Integer; :: thesis: (sgn ((4 * i) + j)) * (Py (a,|.((4 * i) + j).|)),(sgn j) * (Py (a,|.j.|)) are_congruent_mod Px (a,|.i.|)
(4 * i) + j = (2 * i) + ((2 * i) + j) ;
then A1: (sgn ((4 * i) + j)) * (Py (a,|.((4 * i) + j).|)), - ((sgn ((2 * i) + j)) * (Py (a,|.((2 * i) + j).|))) are_congruent_mod Px (a,|.i.|) by Th30;
(- 1) * ((sgn ((2 * i) + j)) * (Py (a,|.((2 * i) + j).|))),(- 1) * (- ((sgn j) * (Py (a,|.j.|)))) are_congruent_mod Px (a,|.i.|) by Th30, INT_4:11;
hence (sgn ((4 * i) + j)) * (Py (a,|.((4 * i) + j).|)),(sgn j) * (Py (a,|.j.|)) are_congruent_mod Px (a,|.i.|) by A1, INT_1:15; :: thesis: verum