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

proof

let k be Nat; :: thesis: ( S₁[k] implies S₁[k + 1] )
Px (a,|.((4 * x) + (((4 * x) * k) + y)).|), Px (a,|.(((4 * x) * k) + y).|) are_congruent_mod Px (a,|.x.|) by Th18;
hence ( S₁[k] implies S₁[k + 1] ) by INT_1:15; :: thesis: verum

end;

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