theorem FIF: :: RVSUM_4:7

for f being non empty complex-valued FinSequence holds Product f = (f . 1) * (Product (f /^ 1))