:: deftheorem Def2 defines Product MESFUNC7:def 2 :
for F being extreal-yielding FinSequence
for b₂ being Element of ExtREAL holds
( b₂ = Product F iff ex f being FinSequence of ExtREAL st
( f = F & b₂ = multextreal $$ f ) );