for S being non empty non void ManySortedSign
for o, a being set
for r being SortSymbol of S st o is_of_type <*a*>,r holds
for A being MSAlgebra over S st the Sorts of A . a <> {} & the Sorts of A . r <> {} holds
for x being Element of the Sorts of A . a holds (Den ((In (o, the carrier' of S)),A)) . <*x*> is Element of the Sorts of A . r