theorem :: MSATERM:12

for S being non empty non void ManySortedSign
for V being non-empty ManySortedSet of the carrier of S
for s being SortSymbol of S holds FreeSort (V,s) c= S -Terms V ;