theorem :: RVSUM_4:15

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