let S be non empty non void ManySortedSign ; :: thesis: for U1 being non-empty MSAlgebra over S
for X being non-empty ManySortedSet of the carrier of S
for h1, h2 being ManySortedFunction of (FreeMSA X),U1 st h1 is_homomorphism FreeMSA X,U1 & h2 is_homomorphism FreeMSA X,U1 & h1 || (FreeGen X) = h2 || (FreeGen X) holds
h1 = h2
let U1 be non-empty MSAlgebra over S; :: thesis: for X being non-empty ManySortedSet of the carrier of S
for h1, h2 being ManySortedFunction of (FreeMSA X),U1 st h1 is_homomorphism FreeMSA X,U1 & h2 is_homomorphism FreeMSA X,U1 & h1 || (FreeGen X) = h2 || (FreeGen X) holds
h1 = h2
let X be non-empty ManySortedSet of the carrier of S; :: thesis: for h1, h2 being ManySortedFunction of (FreeMSA X),U1 st h1 is_homomorphism FreeMSA X,U1 & h2 is_homomorphism FreeMSA X,U1 & h1 || (FreeGen X) = h2 || (FreeGen X) holds
h1 = h2
let h1, h2 be ManySortedFunction of (FreeMSA X),U1; :: thesis: ( h1 is_homomorphism FreeMSA X,U1 & h2 is_homomorphism FreeMSA X,U1 & h1 || (FreeGen X) = h2 || (FreeGen X) implies h1 = h2 )
assume that
A1: h1 is_homomorphism FreeMSA X,U1 and
A2: h2 is_homomorphism FreeMSA X,U1 and
A3: h1 || (FreeGen X) = h2 || (FreeGen X) ; :: thesis: h1 = h2
A4: h2 is_homomorphism FreeMSA X,U1 by A2;
defpred S₁[ SortSymbol of S, set , set ] means (h1 . $1) . $3 = $2;
A5: for s being SortSymbol of S
for x, y being set st y in FreeGen (s,X) holds
( (h2 . s) . y = x iff S₁[s,x,y] )

proof

set FG = FreeGen X;
let s be SortSymbol of S; :: thesis: for x, y being set st y in FreeGen (s,X) holds
( (h2 . s) . y = x iff S₁[s,x,y] )
let x, y be set ; :: thesis: ( y in FreeGen (s,X) implies ( (h2 . s) . y = x iff S₁[s,x,y] ) )
assume y in FreeGen (s,X) ; :: thesis: ( (h2 . s) . y = x iff S₁[s,x,y] )
then A6: y in (FreeGen X) . s by MSAFREE:def 16;
A7: ( (h1 || (FreeGen X)) . s = (h1 . s) | ((FreeGen X) . s) & (h2 || (FreeGen X)) . s = (h2 . s) | ((FreeGen X) . s) ) by MSAFREE:def 1;
((h1 . s) | ((FreeGen X) . s)) . y = (h1 . s) . y by A6, FUNCT_1:49;
hence ( (h2 . s) . y = x iff S₁[s,x,y] ) by A3, A7, A6, FUNCT_1:49; :: thesis: verum

end;

A8: for s being SortSymbol of S
for x, y being set st y in FreeGen (s,X) holds
( (h1 . s) . y = x iff S₁[s,x,y] ) ;
A9: h1 is_homomorphism FreeMSA X,U1 by A1;
thus h1 = h2 from MSAFREE1:sch 3(A9, A8, A4, A5); :: thesis: verum