theorem Lemma2To57: :: NUMBER12:17

for a, b being positive Nat
for k, x, m being Nat st (ArProg (b,a)) . k = x ^2 holds
(ArProg (b,a)) . ((((m ^2) * a) + ((2 * m) * x)) + k) is square