theorem :: NEWTON07:70

for a, b being Complex
for n, k being Nat st k in Seg (n + 1) holds
ex c being object ex l, m being Nat st
( m = k - 1 & l = n - m & c = (a |^ l) * (b |^ m) )