theorem Th12: :: HILB10_8:12

for a being non trivial Nat
for s, n being Nat holds (((s ^2) * ((s |^ n) ^2)) - ((((s ^2) - 1) * (Py (a,(n + 1)))) * (s |^ n))) - 1, 0 are_congruent_mod (((2 * a) * s) - (s ^2)) - 1