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;