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 S1[ 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: S1[ 0 ] by INT_1:11;
A2: for n being Nat st S1[n] holds
S1[n + 1]
proof
let n be Nat; :: thesis: ( S1[n] implies S1[n + 1] )
set n1 = n + 1;
assume A3: S1[n] ; :: thesis: S1[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 S1[n + 1] by A3, INT_1:15; :: thesis: verum
end;
for n being Nat holds S1[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