theorem :: MSATERM:18

for S being non empty non void ManySortedSign
for V being non-empty ManySortedSet of the carrier of S
for A being non-empty MSAlgebra over S
for s being SortSymbol of S
for x being Element of the Sorts of A . s holds the_sort_of (x -term (A,V)) = s by Th15;