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

per cases ( n <> 0 or n = 0 ) ;

suppose n <> 0 ; :: thesis: ex x1, x2, x3, x4 being Nat st n = (((x1 ^2) + (x2 ^2)) + (x3 ^2)) + (x4 ^2)

then reconsider n = n as non zero Nat ;
consider x1, x2, x3, x4 being Nat such that
A1: Product (ppf n) = (((x1 ^2) + (x2 ^2)) + (x3 ^2)) + (x4 ^2) by Them8;
n = (((x1 ^2) + (x2 ^2)) + (x3 ^2)) + (x4 ^2) by A1, NAT_3:61;
hence ex x1, x2, x3, x4 being Nat st n = (((x1 ^2) + (x2 ^2)) + (x3 ^2)) + (x4 ^2) ; :: thesis: verum

end;

suppose A2: n = 0 ; :: thesis: ex x1, x2, x3, x4 being Nat st n = (((x1 ^2) + (x2 ^2)) + (x3 ^2)) + (x4 ^2)

set x1 = 0 ;
set x2 = 0 ;
set x3 = 0 ;
set x4 = 0 ;
n = (((0 ^2) + (0 ^2)) + (0 ^2)) + (0 ^2) by A2;
hence ex x1, x2, x3, x4 being Nat st n = (((x1 ^2) + (x2 ^2)) + (x3 ^2)) + (x4 ^2) ; :: thesis: verum

end;

end;