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