theorem :: MSAFREE5:115

for S being non empty non void ManySortedSign
for s being SortSymbol of S
for Z being non-trivial ManySortedSet of the carrier of S
for z being Element of Z . s
for C9 being context of z holds TranslationRel S reduces s, the_sort_of C9