theorem Prime4Sq: :: LAGRA4SQ:15

for p1, p2 being Prime ex x1, x2, x3, x4 being Nat st p1 * p2 = (((x1 ^2) + (x2 ^2)) + (x3 ^2)) + (x4 ^2)