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 H1( set , set ) -> set = root-tree [$1,(f . $2)];
A2:
now for s being SortSymbol of S1
for x being Element of (X * f) . s holds H1(x,s) in the Sorts of A . slet s be
SortSymbol of
S1;
for x being Element of (X * f) . s holds H1(x,s) in the Sorts of A . slet x be
Element of
(X * f) . s;
H1(x,s) in the Sorts of A . sreconsider 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
H1(
x,
s)
in the
Sorts of
A . s
by A3, FUNCT_2:15;
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 INSTALG1:sch 1(A2);
reconsider G = H as ManySortedFunction of (FreeMSA (X * f)),((FreeMSA X) | (S1,f,g)) ;
take
G
; ( 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; verum