:: deftheorem Def5 defines Product NAT_3:def 5 :
for A being set
for b being complex-valued finite-support ManySortedSet of A
for b₃ being Complex holds
( b₃ = Product b iff ex f being FinSequence of COMPLEX st
( b₃ = Product f & f = b * (canFS (support b)) ) );