let p be Prime; :: thesis: ex x1, x2, x3, x4 being Nat st p = (((x1 ^2) + (x2 ^2)) + (x3 ^2)) + (x4 ^2)

per cases ( p is even or p is odd ) ;

suppose p is even ; :: thesis: ex x1, x2, x3, x4 being Nat st p = (((x1 ^2) + (x2 ^2)) + (x3 ^2)) + (x4 ^2)

hence ex x1, x2, x3, x4 being Nat st p = (((x1 ^2) + (x2 ^2)) + (x3 ^2)) + (x4 ^2) by Them4; :: thesis: verum

end;

suppose p is odd ; :: thesis: ex x1, x2, x3, x4 being Nat st p = (((x1 ^2) + (x2 ^2)) + (x3 ^2)) + (x4 ^2)

hence ex x1, x2, x3, x4 being Nat st p = (((x1 ^2) + (x2 ^2)) + (x3 ^2)) + (x4 ^2) by Them3; :: thesis: verum

end;

end;