:: deftheorem Def5 defines /. UNIALG_2:def 5 :
for U0 being Universal_Algebra
for A being non empty Subset of U0
for o being operation of U0 st A is_closed_on o holds
o /. A = o | ((arity o) -tuples_on A);