theorem Th7: :: HILB10_4:7

for cF1, cF2 being complex-valued XFinSequence holds Product (cF1 ^ cF2) = (Product cF1) * (Product cF2)