let m be Nat; :: thesis: for a1, b1 being Complex holds (a1 |^ (m + 2)) + (b1 |^ (m + 2)) = ((a1 + b1) * ((a1 |^ (m + 1)) + (b1 |^ (m + 1)))) - ((a1 * b1) * ((a1 |^ m) + (b1 |^ m)))
let a1, b1 be Complex; :: thesis: (a1 |^ (m + 2)) + (b1 |^ (m + 2)) = ((a1 + b1) * ((a1 |^ (m + 1)) + (b1 |^ (m + 1)))) - ((a1 * b1) * ((a1 |^ m) + (b1 |^ m)))
( a1 |^ ((m + 1) + 1) = a1 * (a1 |^ (m + 1)) & b1 |^ ((m + 1) + 1) = b1 * (b1 |^ (m + 1)) & a1 |^ (m + 1) = a1 * (a1 |^ m) & b1 |^ (m + 1) = b1 * (b1 |^ m) ) by NEWTON:6;
hence (a1 |^ (m + 2)) + (b1 |^ (m + 2)) = ((a1 + b1) * ((a1 |^ (m + 1)) + (b1 |^ (m + 1)))) - ((a1 * b1) * ((a1 |^ m) + (b1 |^ m))) ; :: thesis: verum