:: deftheorem Def13 defines Product RVSUM_1:def 13 :
for F being complex-valued FinSequence
for b₂ being Complex holds
( b₂ = Product F iff ex f being FinSequence of COMPLEX st
( f = F & b₂ = multcomplex $$ f ) );