:: deftheorem defines is_closed_on UNIALG_2:def 3 :
for U0 being Universal_Algebra
for A being Subset of U0
for o being operation of U0 holds
( A is_closed_on o iff for s being FinSequence of A st len s = arity o holds
o . s in A );