for S being non empty non void ManySortedSign
for X0 being V5() countable ManySortedSet of S
for w being ManySortedFunction of X0, the carrier of S --> NAT st w is "1-1" holds
ex g being ManySortedFunction of (TermAlg S),(Free (S,X0)) st
( g is_homomorphism TermAlg S, Free (S,X0) & ( for s being SortSymbol of S
for t being Element of (Free (S,X0)),s holds (g . s) . (# (t,w)) = t ) )