theorem Them1: :: LAGRA4SQ:6

for p being odd Prime ex x1, x2, x3, x4, h being Nat st
( 0 < h & h < p & h * p = (((x1 ^2) + (x2 ^2)) + (x3 ^2)) + (x4 ^2) )