let S be non empty non void ManySortedSign ; :: thesis: for X being non-empty ManySortedSet of S
for A being b₁,S -terms all_vars_including inheriting_operations free_in_itself MSAlgebra over S
for w being ManySortedFunction of the carrier of S --> NAT,X ex h being ManySortedFunction of (TermAlg S),A st
( h is_homomorphism TermAlg S,A & ( for s being SortSymbol of S
for i being Nat holds (h . s) . (root-tree [i,s]) = root-tree [((w . s) . i),s] ) )
let X be non-empty ManySortedSet of S; :: thesis: for A being X,S -terms all_vars_including inheriting_operations free_in_itself MSAlgebra over S
for w being ManySortedFunction of the carrier of S --> NAT,X ex h being ManySortedFunction of (TermAlg S),A st
( h is_homomorphism TermAlg S,A & ( for s being SortSymbol of S
for i being Nat holds (h . s) . (root-tree [i,s]) = root-tree [((w . s) . i),s] ) )
let A be X,S -terms all_vars_including inheriting_operations free_in_itself MSAlgebra over S; :: thesis: for w being ManySortedFunction of the carrier of S --> NAT,X ex h being ManySortedFunction of (TermAlg S),A st
( h is_homomorphism TermAlg S,A & ( for s being SortSymbol of S
for i being Nat holds (h . s) . (root-tree [i,s]) = root-tree [((w . s) . i),s] ) )
set Y = the carrier of S --> NAT;
let w be ManySortedFunction of the carrier of S --> NAT,X; :: thesis: ex h being ManySortedFunction of (TermAlg S),A st
( h is_homomorphism TermAlg S,A & ( for s being SortSymbol of S
for i being Nat holds (h . s) . (root-tree [i,s]) = root-tree [((w . s) . i),s] ) )
deffunc H₂( set , Function) -> set = root-tree [((w . $1) . (($2 . {}) `1)),$1];
consider ww being ManySortedFunction of the carrier of S such that
A1: for x being set st x in the carrier of S holds
( dom (ww . x) = (FreeGen ( the carrier of S --> NAT)) . x & ( for y being Element of (FreeGen ( the carrier of S --> NAT)) . x holds (ww . x) . y = H₂(x,y) ) ) from MSAFREE4:sch 1();
A2: ww is ManySortedFunction of FreeGen ( the carrier of S --> NAT), FreeGen X

proof

let x be object ; :: according to PBOOLE:def 15 :: thesis: ( not x in the carrier of S or ww . x is Element of bool [:((FreeGen ( the carrier of S --> NAT)) . x),((FreeGen X) . x):] )
assume x in the carrier of S ; :: thesis: ww . x is Element of bool [:((FreeGen ( the carrier of S --> NAT)) . x),((FreeGen X) . x):]
then reconsider s = x as SortSymbol of S ;
A3: dom (ww . s) = (FreeGen ( the carrier of S --> NAT)) . s by A1;
A4: ( (FreeGen X) . s = FreeGen (s,X) & (FreeGen ( the carrier of S --> NAT)) . s = FreeGen (s,( the carrier of S --> NAT)) ) by MSAFREE:def 16;
rng (ww . s) c= (FreeGen X) . s

proof

let y be object ; :: according to TARSKI:def 3 :: thesis: ( not y in rng (ww . s) or y in (FreeGen X) . s )
assume y in rng (ww . s) ; :: thesis: y in (FreeGen X) . s
then consider z being object such that
A5: ( z in dom (ww . s) & y = (ww . s) . z ) by FUNCT_1:def 3;
reconsider z = z as Element of (FreeGen ( the carrier of S --> NAT)) . s by A1, A5;
consider v being set such that
A6: ( v in ( the carrier of S --> NAT) . s & z = root-tree [v,s] ) by A4, MSAFREE:def 15;
A7: y = H₂(s,z) by A1, A5;
z . {} = [v,s] by A6, TREES_4:3;
then (z . {}) `1 = v ;
then (w . s) . ((z . {}) `1) in X . s by A6, FUNCT_2:5;
hence y in (FreeGen X) . s by A4, A7, MSAFREE:def 15; :: thesis: verum

end;

hence ww . x is Element of bool [:((FreeGen ( the carrier of S --> NAT)) . x),((FreeGen X) . x):] by A3, FUNCT_2:2; :: thesis: verum

end;

reconsider G = FreeGen ( the carrier of S --> NAT) as GeneratorSet of TermAlg S ;
FreeGen X is MSSubset of A by Def7;
then reconsider ww = ww as ManySortedFunction of G, the Sorts of A by A2, Th22;
consider h being ManySortedFunction of (TermAlg S),A such that
A8: ( h is_homomorphism TermAlg S,A & ww = h || G ) by MSAFREE:def 5;
take h ; :: thesis: ( h is_homomorphism TermAlg S,A & ( for s being SortSymbol of S
for i being Nat holds (h . s) . (root-tree [i,s]) = root-tree [((w . s) . i),s] ) )
thus h is_homomorphism TermAlg S,A by A8; :: thesis: for s being SortSymbol of S
for i being Nat holds (h . s) . (root-tree [i,s]) = root-tree [((w . s) . i),s]
let s be SortSymbol of S; :: thesis: for i being Nat holds (h . s) . (root-tree [i,s]) = root-tree [((w . s) . i),s]
let i be Nat; :: thesis: (h . s) . (root-tree [i,s]) = root-tree [((w . s) . i),s]
A9: ww . s = (h . s) | (G . s) by A8, MSAFREE:def 1;
( i in NAT & NAT = ( the carrier of S --> NAT) . s ) by ORDINAL1:def 12;
then ( root-tree [i,s] in FreeGen (s,( the carrier of S --> NAT)) & FreeGen (s,( the carrier of S --> NAT)) = G . s ) by MSAFREE:def 15, MSAFREE:def 16;
then reconsider z = root-tree [i,s] as Element of (FreeGen ( the carrier of S --> NAT)) . s ;
thus (h . s) . (root-tree [i,s]) = (ww . s) . z by A9, FUNCT_1:49
.= H₂(s,z) by A1
.= root-tree [((w . s) . ([i,s] `1)),s] by TREES_4:3
.= root-tree [((w . s) . i),s] ; :: thesis: verum