for f being complex-valued FinSequence
for n being Nat holds Product f = (Product (f | n)) * (Product (f /^ n))