theorem Th5: :: NEWTON01:5
for m, n being Nat
for a1, b1 being Complex holds ((((a1 |^ m) + (b1 |^ m)) * ((a1 |^ n) - (b1 |^ n))) + (((a1 |^ n) + (b1 |^ n)) * ((a1 |^ m) - (b1 |^ m)))) / 2 = (a1 |^ (m + n)) - (b1 |^ (m + n))