let n, k be Nat; for a, b being non trivial Nat st a,b are_congruent_mod k holds
Py (a,n), Py (b,n) are_congruent_mod k
let a, b be non trivial Nat; ( a,b are_congruent_mod k implies Py (a,n), Py (b,n) are_congruent_mod k )
assume
a,b are_congruent_mod k
; Py (a,n), Py (b,n) are_congruent_mod k
then consider x being Integer such that
A1:
k * x = a - b
by INT_1:def 5;
consider p being Integer such that
A2:
(a - b) * p = (Py (a,n)) - (Py (b,n))
by Th28, INT_1:def 5;
p * (a - b) =
p * (x * k)
by A1
.=
(p * x) * k
;
hence
Py (a,n), Py (b,n) are_congruent_mod k
by A2, INT_1:def 5; verum