theorem Th1: :: HILB10_4:1

for cF being complex-valued XFinSequence st cF is real-valued holds
Product cF = multreal "**" cF