theorem Them8: :: LAGRA4SQ:17

for n being non zero Nat ex x1, x2, x3, x4 being Nat st Product (ppf n) = (((x1 ^2) + (x2 ^2)) + (x3 ^2)) + (x4 ^2)