theorem :: MSSCYC_1:26

for S being non empty non void ManySortedSign
for X being non-empty ManySortedSet of the carrier of S
for v being SortSymbol of S holds { t where t is Element of the Sorts of (FreeMSA X) . v : depth t = 0 } = (FreeGen (v,X)) \/ (Constants ((FreeMSA X),v))