set A = () | (S1,f,g);
the Sorts of (() | (S1,f,g)) = the Sorts of () * f by ;
then reconsider A = () | (S1,f,g) as non-empty MSAlgebra over S1 by MSUALG_1:def 3;
deffunc H1( set , set ) -> set = root-tree [\$1,(f . \$2)];
A2: now :: thesis: for s being SortSymbol of S1
for x being Element of (X * f) . s holds H1(x,s) in the Sorts of A . s
let s be SortSymbol of S1; :: thesis: for x being Element of (X * f) . s holds H1(x,s) in the Sorts of A . s
let x be Element of (X * f) . s; :: thesis: H1(x,s) in the Sorts of A . s
reconsider fs = f . s as SortSymbol of S2 ;
reconsider y = x as Element of X . fs by FUNCT_2:15;
reconsider t = root-tree [y,fs] as Term of S2,X by MSATERM:4;
the_sort_of t = fs by MSATERM:14;
then t in FreeSort (X,fs) by MSATERM:def 5;
then A3: t in () . fs by MSAFREE:def 11;
( FreeMSA X = MSAlgebra(# (),() #) & the Sorts of A = the Sorts of () * f ) by ;
hence H1(x,s) in the Sorts of A . s by ; :: thesis: verum
end;
consider H being ManySortedFunction of (FreeMSA (X * f)),A such that
A4: ( H is_homomorphism FreeMSA (X * f),A & ( for s being SortSymbol of S1
for x being Element of (X * f) . s holds (H . s) . (root-tree [x,s]) = H1(x,s) ) ) from reconsider G = H as ManySortedFunction of (FreeMSA (X * f)),(() | (S1,f,g)) ;
take G ; :: thesis: ( G is_homomorphism FreeMSA (X * f),() | (S1,f,g) & ( for s being SortSymbol of S1
for x being Element of (X * f) . s holds (G . s) . (root-tree [x,s]) = root-tree [x,(f . s)] ) )

thus ( G is_homomorphism FreeMSA (X * f),() | (S1,f,g) & ( for s being SortSymbol of S1
for x being Element of (X * f) . s holds (G . s) . (root-tree [x,s]) = root-tree [x,(f . s)] ) ) by A4; :: thesis: verum