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_{1}( set , set ) -> set = root-tree [$1,(f . $2)];

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_{1}(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

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

A2: now :: thesis: for s being SortSymbol of S1

for x being Element of (X * f) . s holds H_{1}(x,s) in the Sorts of A . s

consider H being ManySortedFunction of (FreeMSA (X * f)),A such that for x being Element of (X * f) . s holds H

let s be SortSymbol of S1; :: thesis: for x being Element of (X * f) . s holds H_{1}(x,s) in the Sorts of A . s

let x be Element of (X * f) . s; :: thesis: H_{1}(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_{1}(x,s) in the Sorts of A . s
by A3, FUNCT_2:15; :: thesis: verum

end;let x be Element of (X * f) . s; :: thesis: H

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

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

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