let m be Nat; :: thesis: for a1, b1 being Complex holds (a1 |^ (m + 1)) - (b1 |^ (m + 1)) = ((((a1 |^ m) + (b1 |^ m)) * (a1 - b1)) + ((a1 + b1) * ((a1 |^ m) - (b1 |^ m)))) / 2
let a1, b1 be Complex; :: thesis: (a1 |^ (m + 1)) - (b1 |^ (m + 1)) = ((((a1 |^ m) + (b1 |^ m)) * (a1 - b1)) + ((a1 + b1) * ((a1 |^ m) - (b1 |^ m)))) / 2
thus (a1 |^ (m + 1)) - (b1 |^ (m + 1)) = ((((a1 |^ m) + (b1 |^ m)) * (a1 - b1)) + (((a1 |^ 1) + (b1 |^ 1)) * ((a1 |^ m) - (b1 |^ m)))) / 2 by Th5
.= ((((a1 |^ m) + (b1 |^ m)) * (a1 - b1)) + ((a1 + b1) * ((a1 |^ m) - (b1 |^ m)))) / 2 ; :: thesis: verum