theorem :: NUMBER03:61

for k being Nat
for p being Prime st p = (4 * k) + 1 holds
ex a, b being positive Nat st p ^2 = (a ^2) + (b ^2)