theorem Th18: :: MSUALG_9:18

for S being non empty non void ManySortedSign
for A being non-empty MSAlgebra over S
for o being OperSymbol of S
for x being Element of Args (o,A) holds (Den (o,A)) . x in the Sorts of A . (the_result_sort_of o)