theorem :: NEWTON01:3

for a1, b1 being Complex holds ((a1 |^ 2) + (a1 * b1)) + (b1 |^ 2) = ((3 * ((a1 + b1) |^ 2)) + ((a1 - b1) |^ 2)) / 4