:: deftheorem Def6 defines Opers UNIALG_2:def 6 :
for U0 being Universal_Algebra
for A being non empty Subset of U0
for b₃ being PFuncFinSequence of A holds
( b₃ = Opers (U0,A) iff ( dom b₃ = dom the charact of U0 & ( for n being set
for o being operation of U0 st n in dom b₃ & o = the charact of U0 . n holds
b₃ . n = o /. A ) ) );