let a, b be Element of NAT ; :: thesis: (a + b) |^ 2 = (((a * a) + (a * b)) + (a * b)) + (b * b)
(a + b) |^ 2 = (a + b) * (a + b) by WSIERP_1:1
.= (((a * a) + (a * b)) + (b * a)) + (b * b) ;
hence (a + b) |^ 2 = (((a * a) + (a * b)) + (a * b)) + (b * b) ; :: thesis: verum