reconsider A1 = (FreeMSA X) | (S1,f,g) as non-empty MSAlgebra of S1 by A1, Th23;
let G1, G2 be ManySortedFunction of the Sorts of (FreeMSA (X * f)), the Sorts of ((FreeMSA X) | (S1,f,g)); :: thesis:
assume that
A5: G1 is_homomorphism FreeMSA (X * f),(FreeMSA X) | (S1,f,g) and
A6: for s being SortSymbol of S1
for x being Element of (X * f) . s holds (G1 . s) . (root-tree [x,s]) = root-tree [x,(f . s)] and
A7: G2 is_homomorphism FreeMSA (X * f),(FreeMSA X) | (S1,f,g) and
A8: for s being SortSymbol of S1
for x being Element of (X * f) . s holds (G2 . s) . (root-tree [x,s]) = root-tree [x,(f . s)] ; :: thesis:
set H1 = G1;
set H2 = G2;

let x be set ; :: thesis:
assume x in the carrier of S1 ; :: thesis:
then reconsider s = x as SortSymbol of S1 ;
reconsider g1 = (G1 || (FreeGen (X * f))) . s, g2 = (G2 || (FreeGen (X * f))) . s as Function of ((FreeGen (X * f)) . s),( the Sorts of A1 . s) ;

let z be Element of (FreeGen (X * f)) . s; :: thesis:
FreeGen (s,(X * f)) = (FreeGen (X * f)) . s by MSAFREE:def 18;
then consider a being set such that
A10: a in (X * f) . s and
A11: z = root-tree [a,s] by MSAFREE:def 17;
reconsider a = a as Element of (X * f) . s by A10;
thus g1 . z = (G1 . s) . z by Th40
.= root-tree [a,(f . s)] by A6, A11
.= (G2 . s) . z by A8, A11
.= g2 . z by Th40 ; :: thesis:

end;

end;