:: deftheorem defines [[: PRALG_1:def 22 :
for J being non empty set
for B being non-empty ManySortedSet of J
for O being equal-arity ManySortedOperation of B
for b₄ being non empty homogeneous quasi_total PartFunc of ((product B) *),(product B) holds
( b₄ = [[:O:]] iff ( dom b₄ = (ComAr O) -tuples_on (product B) & ( for p being Element of (product B) * st p in dom b₄ holds
( ( dom p = {} implies b₄ . p = O .. (EmptyMS J) ) & ( dom p <> {} implies for Z being non empty set
for w being ManySortedSet of [:J,Z:] st Z = dom p & w = ~ (uncurry p) holds
b₄ . p = O .. (curry w) ) ) ) ) );