theorem Th4: :: NUMBER15:4

for a being Complex
for p, q being complex-valued FinSequence st len p = len q & ex i being Nat st
( i in dom p & q . i = a * (p . i) & ( for j being Nat st j in dom p & i <> j holds
q . j = p . j ) ) holds
Product q = a * (Product p)