:: deftheorem Def8 defines Opers MSUALG_2:def 8 :
for S being non empty non void ManySortedSign
for U0 being MSAlgebra over S
for A being MSSubset of U0
for b₄ being ManySortedFunction of (A #) * the Arity of S,A * the ResultSort of S holds
( b₄ = Opers (U0,A) iff for o being OperSymbol of S holds b₄ . o = o /. A );