:: deftheorem defines OPS PRALG_2:def 13 :
for I being set
for S being non empty non void ManySortedSign
for A being MSAlgebra-Family of I,S
for b₄ being ManySortedFunction of ((SORTS A) #) * the Arity of S,(SORTS A) * the ResultSort of S holds
( ( I <> {} implies ( b₄ = OPS A iff for o being OperSymbol of S holds b₄ . o = IFEQ ((the_arity_of o),{},(commute (A ?. o)),(Commute (Frege (A ?. o)))) ) ) & ( not I <> {} implies ( b₄ = OPS A iff verum ) ) );