(0 ^2) + (0 ^2) = (0 * 0) + (0 ^2) by SQUARE_1:def 1
.= 0 * 0 by SQUARE_1:def 1 ;
hence (0 ^2) + (0 ^2) = 0 ; :: thesis: verum