for a, b being Element of NAT holds (a + b) |^ 2 = (((a * a) + (a * b)) + (a * b)) + (b * b)