theorem Th38: :: HILB10_1:35

for n, k being Nat
for a being non trivial Nat holds Py (a,(n * k)),(k * ((Px (a,n)) |^ (k -' 1))) * (Py (a,n)) are_congruent_mod (Py (a,n)) ^2