let n be Nat; :: thesis: for x, y being Integer
for a being non trivial Nat holds (sgn (((4 * x) * n) + y)) * (Py (a,|.(((4 * x) * n) + y).|)),(sgn y) * (Py (a,|.y.|)) are_congruent_mod Px (a,|.x.|)
let x, y be Integer; :: thesis: for a being non trivial Nat holds (sgn (((4 * x) * n) + y)) * (Py (a,|.(((4 * x) * n) + y).|)),(sgn y) * (Py (a,|.y.|)) are_congruent_mod Px (a,|.x.|)
let a be non trivial Nat; :: thesis: (sgn (((4 * x) * n) + y)) * (Py (a,|.(((4 * x) * n) + y).|)),(sgn y) * (Py (a,|.y.|)) are_congruent_mod Px (a,|.x.|)
defpred S₁[ Nat] means (sgn (((4 * x) * $1) + y)) * (Py (a,|.(((4 * x) * $1) + y).|)),(sgn y) * (Py (a,|.y.|)) are_congruent_mod Px (a,|.x.|);
A1: S₁[ 0 ] by INT_1:11;
A2: for n being Nat st S₁[n] holds
S₁[n + 1]

proof

let n be Nat; :: thesis: ( S₁[n] implies S₁[n + 1] )
set n1 = n + 1;
assume A3: S₁[n] ; :: thesis: S₁[n + 1]
((4 * x) * (n + 1)) + y = (4 * x) + (((4 * x) * n) + y) ;
then (sgn (((4 * x) * (n + 1)) + y)) * (Py (a,|.(((4 * x) * (n + 1)) + y).|)),(sgn (((4 * x) * n) + y)) * (Py (a,|.(((4 * x) * n) + y).|)) are_congruent_mod Px (a,|.x.|) by Lm7;
hence S₁[n + 1] by A3, INT_1:15; :: thesis: verum

end;

for n being Nat holds S₁[n] from NAT_1:sch 2(A1, A2);
hence (sgn (((4 * x) * n) + y)) * (Py (a,|.(((4 * x) * n) + y).|)),(sgn y) * (Py (a,|.y.|)) are_congruent_mod Px (a,|.x.|) ; :: thesis: verum