:: deftheorem defines is_closed_on MSUALG_2:def 5 :
for S being non empty non void ManySortedSign
for U0 being MSAlgebra over S
for o being OperSymbol of S
for A being MSSubset of U0 holds
( A is_closed_on o iff rng ((Den (o,U0)) | (((A #) * the Arity of S) . o)) c= (A * the ResultSort of S) . o );