let k, m be Nat; :: thesis: for a1, b1 being Complex st (a1 |^ (m + 2)) - (b1 |^ (m + 2)) = (((a1 |^ (m + 1)) + (b1 |^ (m + 1))) + ((a1 * b1) * k)) * (a1 - b1) & a1 * b1 <> 0 holds
(a1 |^ m) - (b1 |^ m) = (a1 - b1) * k
let a1, b1 be Complex; :: thesis: ( (a1 |^ (m + 2)) - (b1 |^ (m + 2)) = (((a1 |^ (m + 1)) + (b1 |^ (m + 1))) + ((a1 * b1) * k)) * (a1 - b1) & a1 * b1 <> 0 implies (a1 |^ m) - (b1 |^ m) = (a1 - b1) * k )
assume A1: ( (a1 |^ (m + 2)) - (b1 |^ (m + 2)) = (((a1 |^ (m + 1)) + (b1 |^ (m + 1))) + ((a1 * b1) * k)) * (a1 - b1) & a1 * b1 <> 0 ) ; :: thesis: (a1 |^ m) - (b1 |^ m) = (a1 - b1) * k
then A5: ((k * (a1 - b1)) * (a1 * b1)) / (a1 * b1) = k * (a1 - b1) by XCMPLX_1:89;
(((a1 |^ (m + 1)) + (b1 |^ (m + 1))) * (a1 - b1)) + ((a1 * b1) * ((a1 |^ m) - (b1 |^ m))) = (((a1 |^ (m + 1)) + (b1 |^ (m + 1))) * (a1 - b1)) + (((a1 * b1) * k) * (a1 - b1)) by A1, Th21;
hence (a1 |^ m) - (b1 |^ m) = (a1 - b1) * k by A1, XCMPLX_1:89, A5; :: thesis: verum