for S being non empty non void ManySortedSign
for X0 being V5() countable ManySortedSet of S
for B being non-empty MSAlgebra over S
for h being ManySortedFunction of (Free (S,X0)),B st h is_homomorphism Free (S,X0),B holds
for w being ManySortedFunction of X0, the carrier of S --> NAT st w is "1-1" holds
for s being SortSymbol of S
for t1, t2 being Element of (Free (S,X0)),s
for t3, t4 being Element of (TermAlg S),s st t3 = # (t1,w) & t4 = # (t2,w) & B |= t3 '=' t4 holds
(h . s) . t1 = (h . s) . t2