theorem Th4: :: HILB10_4:4

for cF being complex-valued XFinSequence st cF = {} holds
Product cF = 1