theorem Them5: :: LAGRA4SQ:12

for p being odd Prime
for x1, x2, x3, x4, h being Nat st 1 < h & h < p & h * p = (((x1 ^2) + (x2 ^2)) + (x3 ^2)) + (x4 ^2) holds
ex y1, y2, y3, y4 being Integer ex r being Nat st
( 0 < r & r < h & r * p = (((y1 ^2) + (y2 ^2)) + (y3 ^2)) + (y4 ^2) )