theorem :: SQUARE_1:6

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