:: deftheorem Def11 defines OPER PRALG_2:def 11 :
for I being set
for S being non empty ManySortedSign
for A being MSAlgebra-Family of I,S
for b₄ being ManySortedFunction of I holds
( ( I <> {} implies ( b₄ = OPER A iff for i being set st i in I holds
ex U0 being MSAlgebra over S st
( U0 = A . i & b₄ . i = the Charact of U0 ) ) ) & ( not I <> {} implies ( b₄ = OPER A iff b₄ = {} ) ) );