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