let p be odd Prime; :: thesis: ex x1, x2, x3, x4 being Nat st p = (((x1 ^2) + (x2 ^2)) + (x3 ^2)) + (x4 ^2)
defpred S₁[ Nat] means ex x1, x2, x3, x4 being Integer st
( 0 < $1 & $1 < p & $1 * p = (((x1 ^2) + (x2 ^2)) + (x3 ^2)) + (x4 ^2) );
A1: ex h being Nat st S₁[h]

proof

consider x1, x2, x3, x4, h1 being Nat such that
A3: h1 > 0 and
A4: h1 < p and
A5: h1 * p = (((x1 ^2) + (x2 ^2)) + (x3 ^2)) + (x4 ^2) by Them1;
thus ex h being Nat st S₁[h] by A3, A4, A5; :: thesis: verum

end;

A7: ex h being Nat st
( S₁[h] & ( for n being Nat st S₁[n] holds
h <= n ) ) from NAT_1:sch 5(A1);
consider h0 being Nat such that
A8: S₁[h0] and
A9: for n being Nat st S₁[n] holds
h0 <= n by A7;
consider x1, x2, x3, x4 being Integer such that
A11: h0 * p = (((x1 ^2) + (x2 ^2)) + (x3 ^2)) + (x4 ^2) by A8;
A13: h0 >= 0 + 1 by A8, INT_1:7;
reconsider z1 = |.x1.|, z2 = |.x2.|, z3 = |.x3.|, z4 = |.x4.| as natural set by TARSKI:1;
A16: ( z1 ^2 = x1 ^2 & z2 ^2 = x2 ^2 & z3 ^2 = x3 ^2 & z4 ^2 = x4 ^2 ) by COMPLEX1:75;
h0 = 1

proof

assume A19: h0 <> 1 ; :: thesis: contradiction

per cases ( h0 > 1 or h0 < 1 ) by A19, XXREAL_0:1;

suppose A21: h0 > 1 ; :: thesis: contradiction

consider y1, y2, y3, y4 being Integer, h1 being Nat such that
A23: 0 < h1 and
A24: h1 < h0 and
A25: h1 * p = (((y1 ^2) + (y2 ^2)) + (y3 ^2)) + (y4 ^2) by A8, A11, A16, A21, Them5;
h1 < p by A24, A8, XXREAL_0:2;
hence contradiction by A9, A23, A24, A25; :: thesis: verum

end;

suppose h0 < 1 ; :: thesis: contradiction

hence contradiction by A13; :: thesis: verum

end;

end;

end;

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