theorem Th6: :: HURWITZ:6

for F, G being FinSequence of F_Complex st len G = len F & ( for i being Element of NAT st i in dom G holds
G /. i = (F /. i) *' ) holds
Sum G = (Sum F) *'