theorem Th30: :: OSAFREE:30

for S being locally_directed OrderSortedSign
for X being non-empty ManySortedSet of S
for s being Element of S holds OSFreeGen (s,X) = { (((OSNat_Hom ((ParsedTermsOSA X),(LCongruence X))) . s) . (root-tree t)) where t is Symbol of (DTConOSA X) : ( t in Terminals (DTConOSA X) & t `2 = s ) }