:: deftheorem Def15 defines ManySortedOperation PRALG_1:def 17 :
for J being non empty set
for B being non-empty ManySortedSet of J
for b₃ being ManySortedFunction of J holds
( b₃ is ManySortedOperation of B iff for j being Element of J holds b₃ . j is non empty homogeneous quasi_total PartFunc of ((B . j) *),(B . j) );