theorem Them7: :: LAGRA4SQ:16

for p being Prime
for n being Nat ex x1, x2, x3, x4 being Nat st p |^ n = (((x1 ^2) + (x2 ^2)) + (x3 ^2)) + (x4 ^2)