theorem :: MSAFREE4:64

for S being non empty non void ManySortedSign
for X0 being non-empty countable ManySortedSet of S
for A0 being b₂,b₁ -terms all_vars_including inheriting_operations free_in_itself MSAlgebra over S
for h being ManySortedFunction of (TermAlg S),A0 st h is_homomorphism TermAlg S,A0 holds
for w being ManySortedFunction of X0, the carrier of S --> NAT st w is "1-1" holds
ex Y being non-empty ManySortedSubset of the carrier of S --> NAT ex B being MSSubset of (TermAlg S) ex ww being ManySortedFunction of (Free (S,Y)),A0 ex g being ManySortedFunction of A0,A0 st
( Y = rngs w & B = the Sorts of (Free (S,Y)) & FreeGen (rngs w) c= B & ww is_homomorphism Free (S,Y),A0 & g is_homomorphism A0,A0 & h || B = g ** ww & ( for s being SortSymbol of S
for i being Nat st i in Y . s holds
ex x being Element of X0 . s st
( (w . s) . x = i & (ww . s) . (root-tree [i,s]) = root-tree [x,s] ) ) )