theorem Th3: :: HILB10_4:3

for cF being complex-valued XFinSequence st cF is natural-valued holds
Product cF = multnat "**" cF