let a1, b1 be Complex; :: thesis: (a1 + b1) |^ 2 = ((a1 |^ 2) + ((2 * a1) * b1)) + (b1 |^ 2)
( (a1 + b1) |^ 2 = (a1 + b1) ^2 & a1 |^ 2 = a1 ^2 & b1 |^ 2 = b1 ^2 ) by NEWTON:81;
hence (a1 + b1) |^ 2 = ((a1 |^ 2) + ((2 * a1) * b1)) + (b1 |^ 2) by SQUARE_1:4; :: thesis: verum