for S being non empty non void ManySortedSign
for o being OperSymbol of S
for U0 being MSAlgebra over S
for A being MSSubset of U0 holds rng ((Den (o,U0)) | ((((MSSubSort A) #) * the Arity of S) . o)) c= ((MSSubSort A) * the ResultSort of S) . o