theorem :: MSAFREE5:125

for S being non empty non void ManySortedSign
for s1 being SortSymbol of S
for Y being infinite-yielding ManySortedSet of the carrier of S
for s2 being b₂ -reachable SortSymbol of S
for g1 being Translation of Free (S,Y),s1,s2 ex y11 being Element of Y . s1 ex C12 being context of y11 st
( the_sort_of C12 = s2 & g1 = transl C12 )