theorem :: SQUARE_1:4

for a, b being Complex holds (a + b) ^2 = ((a ^2) + ((2 * a) * b)) + (b ^2) ;