:: deftheorem Def5 defines # FINSEQ_2:def 5 :
for I being set
for M being ManySortedSet of I
for b₃ being ManySortedSet of I * holds
( b₃ = M # iff for i being Element of I * holds b₃ . i = product (M * i) );