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