theorem :: NAT_5:23

for p being Nat st p is prime & p mod 4 = 1 holds
ex n, m being Nat st p = (n ^2) + (m ^2)