theorem :: NEWTON01:7

for n being Nat
for a1, b1, c1 being Complex st (a1 + b1) |^ (n + 1) = ((a1 |^ (n + 1)) + (b1 |^ (n + 1))) + ((a1 * b1) * c1) holds
(a1 + b1) |^ (n + 2) = ((a1 |^ (n + 2)) + (b1 |^ (n + 2))) + ((a1 * b1) * (((a1 |^ n) + (b1 |^ n)) + (c1 * (a1 + b1))))