take n = 0 ; :: thesis: n is a_sum_of_four_squares
take 0 ; :: according to LAGRA4SQ:def 1 :: thesis: ex n2, n3, n4 being Nat st n = (((0 ^2) + (n2 ^2)) + (n3 ^2)) + (n4 ^2)
take 0 ; :: thesis: ex n3, n4 being Nat st n = (((0 ^2) + (0 ^2)) + (n3 ^2)) + (n4 ^2)
take 0 ; :: thesis: ex n4 being Nat st n = (((0 ^2) + (0 ^2)) + (0 ^2)) + (n4 ^2)
take 0 ; :: thesis: n = (((0 ^2) + (0 ^2)) + (0 ^2)) + (0 ^2)
thus n = (((0 ^2) + (0 ^2)) + (0 ^2)) + (0 ^2) ; :: thesis: verum