theorem :: MSATERM:13

for S being non empty non void ManySortedSign
for V being non-empty ManySortedSet of the carrier of S holds S -Terms V = Union (FreeSort V)