let S be non empty non void ManySortedSign ; :: thesis: for X being non-empty ManySortedSet of S
for w being ManySortedFunction of X, the carrier of S --> NAT ex h being ManySortedFunction of FreeGen X, the Sorts of (TermAlg S) st
for s being SortSymbol of S
for i being Element of X . s holds (h . s) . (root-tree [i,s]) = root-tree [((w . s) . i),s]
let X be non-empty ManySortedSet of S; :: thesis: for w being ManySortedFunction of X, the carrier of S --> NAT ex h being ManySortedFunction of FreeGen X, the Sorts of (TermAlg S) st
for s being SortSymbol of S
for i being Element of X . s 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 X, the carrier of S --> NAT; :: thesis: ex h being ManySortedFunction of FreeGen X, the Sorts of (TermAlg S) st
for s being SortSymbol of S
for i being Element of X . s 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 X) . x & ( for y being Element of (FreeGen X) . x holds (ww . x) . y = H₂(x,y) ) ) from MSAFREE4:sch 1();
A2: ww is ManySortedFunction of FreeGen X, FreeGen ( the carrier of S --> NAT)

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 X) . x),((FreeGen ( the carrier of S --> NAT)) . x):] )
assume x in the carrier of S ; :: thesis: ww . x is Element of bool [:((FreeGen X) . x),((FreeGen ( the carrier of S --> NAT)) . x):]
then reconsider s = x as SortSymbol of S ;
A3: dom (ww . s) = (FreeGen X) . 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 ( the carrier of S --> NAT)) . s

proof

let y be object ; :: according to TARSKI:def 3 :: thesis: ( not y in rng (ww . s) or y in (FreeGen ( the carrier of S --> NAT)) . s )
assume y in rng (ww . s) ; :: thesis: y in (FreeGen ( the carrier of S --> NAT)) . 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 X) . s by A1, A5;
consider v being set such that
A6: ( v in X . 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 ( the carrier of S --> NAT) . s by A6, FUNCT_2:5;
hence y in (FreeGen ( the carrier of S --> NAT)) . s by A4, A7, MSAFREE:def 15; :: thesis: verum

end;

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

end;

set A = the X,S -terms all_vars_including inheriting_operations free_in_itself MSAlgebra over S;
reconsider G = FreeGen X as GeneratorSet of the X,S -terms all_vars_including inheriting_operations free_in_itself MSAlgebra over S by Th45;
reconsider ww = ww as ManySortedFunction of FreeGen X, the Sorts of (TermAlg S) by A2, Th22;
take ww ; :: thesis: for s being SortSymbol of S
for i being Element of X . s holds (ww . s) . (root-tree [i,s]) = root-tree [((w . s) . i),s]
let s be SortSymbol of S; :: thesis: for i being Element of X . s holds (ww . s) . (root-tree [i,s]) = root-tree [((w . s) . i),s]
let i be Element of X . s; :: thesis: (ww . s) . (root-tree [i,s]) = root-tree [((w . s) . i),s]
( root-tree [i,s] in FreeGen (s,X) & FreeGen (s,X) = G . s ) by MSAFREE:def 15, MSAFREE:def 16;
then reconsider z = root-tree [i,s] as Element of (FreeGen X) . s ;
thus (ww . s) . (root-tree [i,s]) = 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