let G1, G2 be ManySortedFunction of the Sorts of (FreeMSA (X * f)),the Sorts of ((FreeMSA X) | S1,f,g); :: thesis: ( G1 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 (G1 . s) . (root-tree [x,s]) = root-tree [x,(f . s)] ) & G2 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 (G2 . s) . (root-tree [x,s]) = root-tree [x,(f . s)] ) implies G1 = G2 )
assume that
A6: G1 is_homomorphism FreeMSA (X * f),(FreeMSA X) | S1,f,g and
A7: 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
A8: G2 is_homomorphism FreeMSA (X * f),(FreeMSA X) | S1,f,g and
A9: 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: G1 = G2
set H1 = G1;
set H2 = G2;
reconsider A1 = (FreeMSA X) | S1,f,g as non-empty MSAlgebra of S1 by A1, Th23;

now

let x be set ; :: thesis: ( x in the carrier of S1 implies (G1 || (FreeGen (X * f))) . x = (G2 || (FreeGen (X * f))) . x )
assume x in the carrier of S1 ; :: thesis: (G1 || (FreeGen (X * f))) . x = (G2 || (FreeGen (X * f))) . x
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) ;

now

let z be Element of (FreeGen (X * f)) . s; :: thesis: g1 . z = g2 . z
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 & 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 A7, A10
.= (G2 . s) . z by A9, A10
.= g2 . z by Th40 ; :: thesis: verum

end;

hence (G1 || (FreeGen (X * f))) . x = (G2 || (FreeGen (X * f))) . x by FUNCT_2:113; :: thesis: verum

end;

then ( G1 || (FreeGen (X * f)) = G2 || (FreeGen (X * f)) & A1 = (FreeMSA X) | S1,f,g ) by PBOOLE:3;
hence G1 = G2 by A6, A8, EXTENS_1:18; :: thesis: verum