set A = (FreeMSA X) | (S1,f,g);
the Sorts of ((FreeMSA X) | (S1,f,g)) = the Sorts of (FreeMSA X) * f by A1, Def3;
then reconsider A = (FreeMSA X) | (S1,f,g) as non-empty MSAlgebra over S1 by MSUALG_1:def 3;
deffunc H₁( 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 H₁(x,s) in the Sorts of A . s

let s be SortSymbol of S1; :: thesis: for x being Element of (X * f) . s holds H₁(x,s) in the Sorts of A . s
let x be Element of (X * f) . s; :: thesis: H₁(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 (FreeSort X) . fs by MSAFREE:def 11;
( FreeMSA X = MSAlgebra(# (FreeSort X),(FreeOper X) #) & the Sorts of A = the Sorts of (FreeMSA X) * f ) by A1, Def3, MSAFREE:def 14;
hence H₁(x,s) in the Sorts of A . s by A3, FUNCT_2:15; :: 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]) = H₁(x,s) ) ) from INSTALG1:sch 1(A2);
reconsider G = H as ManySortedFunction of (FreeMSA (X * f)),((FreeMSA X) | (S1,f,g)) ;
take G ; :: thesis: ( G is_homomorphism FreeMSA (X * f),(FreeMSA X) | (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),(FreeMSA X) | (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