:: deftheorem defines Product HILB10_4:def 1 :
for cF being XFinSequence holds Product cF = multcomplex "**" cF;