let p be Prime; :: thesis: ( p is even implies ex x1, x2, x3, x4 being Nat st p = (((x1 ^2) + (x2 ^2)) + (x3 ^2)) + (x4 ^2) )
assume A1: p is even ; :: thesis: ex x1, x2, x3, x4 being Nat st p = (((x1 ^2) + (x2 ^2)) + (x3 ^2)) + (x4 ^2)
reconsider p = p as Integer ;
set x1 = 1;
set x2 = 1;
set x3 = 0 ;
set x4 = 0 ;
p = (((1 ^2) + (1 ^2)) + (0 ^2)) + (0 ^2) by A1, ABIAN:def 1, INT_2:def 4;
hence ex x1, x2, x3, x4 being Nat st p = (((x1 ^2) + (x2 ^2)) + (x3 ^2)) + (x4 ^2) ; :: thesis: verum