theorem Th13: :: MSAFREE:13

for S being non empty non void ManySortedSign
for X being non-empty ManySortedSet of the carrier of S
for s being SortSymbol of S holds FreeGen (s,X) = { (root-tree t) where t is Symbol of (DTConMSA X) : ( t in Terminals (DTConMSA X) & t `2 = s ) }