theorem :: MSAFREE:15

for S being non empty non void ManySortedSign
for X being non-empty ManySortedSet of the carrier of S holds union (rng (FreeGen X)) = { (root-tree t) where t is Symbol of (DTConMSA X) : t in Terminals (DTConMSA X) }