:: deftheorem defines ProdOp PRALG_1:def 23 :
for J being non empty set
for A being Univ_Alg-yielding equal-signature ManySortedSet of J
for n being Nat st n in dom (ComSign A) holds
for b₄ being equal-arity ManySortedOperation of Carrier A holds
( b₄ = ProdOp (A,n) iff for j being Element of J
for o being operation of (A . j) st the charact of (A . j) . n = o holds
b₄ . j = o );