let k, n be Nat; :: thesis: for a1, b1 being Complex holds (a1 |^ (n + k)) - (b1 |^ (n + k)) = ((a1 |^ n) * ((a1 |^ k) - (b1 |^ k))) + ((b1 |^ k) * ((a1 |^ n) - (b1 |^ n)))
let a1, b1 be Complex; :: thesis: (a1 |^ (n + k)) - (b1 |^ (n + k)) = ((a1 |^ n) * ((a1 |^ k) - (b1 |^ k))) + ((b1 |^ k) * ((a1 |^ n) - (b1 |^ n)))
( a1 |^ (n + k) = (a1 |^ n) * (a1 |^ k) & b1 |^ (n + k) = (b1 |^ n) * (b1 |^ k) ) by NEWTON:8;
hence (a1 |^ (n + k)) - (b1 |^ (n + k)) = ((a1 |^ n) * ((a1 |^ k) - (b1 |^ k))) + ((b1 |^ k) * ((a1 |^ n) - (b1 |^ n))) ; :: thesis: verum