let S be non empty non void ManySortedSign ; :: thesis:
let U2, U3 be non-empty MSAlgebra of S; :: thesis:
let F be ManySortedFunction of U2,U3; :: thesis:
assume A1: F is_homomorphism U2,U3 ; :: thesis:
thus ( F is_monomorphism U2,U3 implies for U1 being non-empty MSAlgebra of S
for h1, h2 being ManySortedFunction of U1,U2 st h1 is_homomorphism U1,U2 & h2 is_homomorphism U1,U2 & F ** h1 = F ** h2 holds
h1 = h2 ) :: thesis:

proof

assume F is_monomorphism U2,U3 ; :: thesis:
then F is "1-1" by MSUALG_3:def 11;
hence for U1 being non-empty MSAlgebra of S
for h1, h2 being ManySortedFunction of U1,U2 st h1 is_homomorphism U1,U2 & h2 is_homomorphism U1,U2 & F ** h1 = F ** h2 holds
h1 = h2 by Th17; :: thesis:

end;

assume that
A2: for U1 being non-empty MSAlgebra of S
for h1, h2 being ManySortedFunction of U1,U2 st h1 is_homomorphism U1,U2 & h2 is_homomorphism U1,U2 & F ** h1 = F ** h2 holds
h1 = h2 and
A3: not F is_monomorphism U2,U3 ; :: thesis:
set I = the carrier of S;
not F is "1-1" by A1, A3, MSUALG_3:def 11;
then consider j being set such that
A4: ( j in the carrier of S & not F . j is one-to-one ) by MSUALG_3:1;
set B = the Sorts of U2;
set C = the Sorts of U3;
A5: F . j is Function of (the Sorts of U2 . j),(the Sorts of U3 . j) by A4, PBOOLE:def 18;
set f = F . j;
consider x1, x2 being set such that
A6: ( x1 in the Sorts of U2 . j & x2 in the Sorts of U2 . j & (F . j) . x1 = (F . j) . x2 & x1 <> x2 ) by A4, A5, FUNCT_2:25;
ex U1 being non-empty MSAlgebra of S ex h1, h2 being ManySortedFunction of the Sorts of U1,the Sorts of U2 st
( h1 is_homomorphism U1,U2 & h2 is_homomorphism U1,U2 & F ** h1 = F ** h2 & h1 <> h2 )

proof

take U1 = FreeMSA the Sorts of U2; :: thesis:
reconsider FG = FreeGen the Sorts of U2 as GeneratorSet of U1 ;
A7: FG is free by MSAFREE:17;
set r = Reverse the Sorts of U2;
FG is non-empty by MSAFREE:15;
then reconsider FGj = FG . j, Bj = the Sorts of U2 . j as non empty set by A4;
reconsider g = FGj --> x1 as Function of FGj,Bj by A6, FUNCOP_1:57;
reconsider h = FGj --> x2 as Function of FGj,Bj by A6, FUNCOP_1:57;
deffunc H₁( set ) -> set = IFEQ $1,j,g,((Reverse the Sorts of U2) . $1);
consider G being ManySortedSet of such that
A8: for i being set st i in the carrier of S holds
G . i = H₁(i) from PBOOLE:sch 4();
deffunc H₂( set ) -> set = IFEQ $1,j,h,((Reverse the Sorts of U2) . $1);
consider H being ManySortedSet of such that
A9: for i being set st i in the carrier of S holds
H . i = H₂(i) from PBOOLE:sch 4();

now

let G be ManySortedSet of ; :: thesis:
let g, h be Function of FGj,Bj; :: thesis:
assume A10: for i being set st i in the carrier of S holds
G . i = IFEQ i,j,g,((Reverse the Sorts of U2) . i) ; :: thesis:
thus G is Function-yielding :: thesis:

proof

let i be set ; :: according to FUNCOP_1:def 6 :: thesis:
assume i in dom G ; :: thesis:
then A11: i in the carrier of S by PARTFUN1:def 4;

now

per cases ;

case i = j ; :: thesis:

then IFEQ i,j,g,((Reverse the Sorts of U2) . i) = g by FUNCOP_1:def 8;
hence G . i is set by A10, A11; :: thesis:

end;

case i <> j ; :: thesis:

then IFEQ i,j,g,((Reverse the Sorts of U2) . i) = (Reverse the Sorts of U2) . i by FUNCOP_1:def 8;
hence G . i is set by A10, A11; :: thesis:

end;

hence G . i is set ; :: thesis:

end;

then reconsider G = G, H = H as ManySortedFunction of by A8, A9;

now

let G be ManySortedFunction of ; :: thesis:
let g, h be Function of FGj,Bj; :: thesis:
assume A12: for i being set st i in the carrier of S holds
G . i = IFEQ i,j,g,((Reverse the Sorts of U2) . i) ; :: thesis:
thus G is ManySortedFunction of FG,the Sorts of U2 :: thesis:

proof

let i be set ; :: according to PBOOLE:def 18 :: thesis:
assume A13: i in the carrier of S ; :: thesis:

now

per cases ;

case A14: i = j ; :: thesis:

then IFEQ i,j,g,((Reverse the Sorts of U2) . i) = g by FUNCOP_1:def 8;
hence G . i is Element of K21(K22((FG . i),(the Sorts of U2 . i))) by A12, A13, A14; :: thesis:

end;

case i <> j ; :: thesis:

then IFEQ i,j,g,((Reverse the Sorts of U2) . i) = (Reverse the Sorts of U2) . i by FUNCOP_1:def 8;
then G . i = (Reverse the Sorts of U2) . i by A12, A13;
hence G . i is Element of K21(K22((FG . i),(the Sorts of U2 . i))) by A13, PBOOLE:def 18; :: thesis:

end;

hence G . i is Element of K21(K22((FG . i),(the Sorts of U2 . i))) ; :: thesis:

end;

then reconsider G = G, H = H as ManySortedFunction of FG,the Sorts of U2 by A8, A9;
consider h1 being ManySortedFunction of U1,U2 such that
A15: ( h1 is_homomorphism U1,U2 & h1 || FG = G ) by A7, MSAFREE:def 5;
consider h2 being ManySortedFunction of U1,U2 such that
A16: ( h2 is_homomorphism U1,U2 & h2 || FG = H ) by A7, MSAFREE:def 5;
take h1 ; :: thesis:
take h2 ; :: thesis:
thus ( h1 is_homomorphism U1,U2 & h2 is_homomorphism U1,U2 ) by A15, A16; :: thesis:

now

let i be set ; :: thesis:
assume A17: i in the carrier of S ; :: thesis:

now

per cases ;

case A18: i = j ; :: thesis:

then A19: IFEQ i,j,g,((Reverse the Sorts of U2) . i) = g by FUNCOP_1:def 8;
A20: IFEQ i,j,h,((Reverse the Sorts of U2) . i) = h by A18, FUNCOP_1:def 8;
A21: F . j is Function of (the Sorts of U2 . i),(the Sorts of U3 . i) by A4, A18, PBOOLE:def 18;
then reconsider fg = (F . j) * g as Function of FGj,(the Sorts of U3 . i) by A18, FUNCT_2:19;
reconsider fh = (F . j) * h as Function of FGj,(the Sorts of U3 . i) by A18, A21, FUNCT_2:19;

now

let x be set ; :: thesis:
assume A22: x in FGj ; :: thesis:
hence fg . x = (F . j) . (g . x) by FUNCT_2:21
.= (F . j) . x2 by A6, A22, FUNCOP_1:13
.= (F . j) . (h . x) by A22, FUNCOP_1:13
.= fh . x by A22, FUNCT_2:21 ;
:: thesis:

end;

then A23: (F . j) * g = (F . j) * h by FUNCT_2:18;
A24: h = (h2 || FG) . i by A9, A16, A17, A20;
g = (h1 || FG) . i by A8, A15, A17, A19;
then (F ** (h1 || FG)) . i = (F . j) * g by A4, A18, MSUALG_3:2;
hence (F ** (h1 || FG)) . i = (F ** (h2 || FG)) . i by A4, A18, A23, A24, MSUALG_3:2; :: thesis:

end;

case A25: i <> j ; :: thesis:

then A26: IFEQ i,j,g,((Reverse the Sorts of U2) . i) = (Reverse the Sorts of U2) . i by FUNCOP_1:def 8;
A27: IFEQ i,j,h,((Reverse the Sorts of U2) . i) = (Reverse the Sorts of U2) . i by A25, FUNCOP_1:def 8;
A28: (h1 || FG) . i = (Reverse the Sorts of U2) . i by A8, A15, A17, A26
.= (h2 || FG) . i by A9, A16, A17, A27 ;
reconsider h2' = (h2 || FG) . i as Function of (FG . i),(the Sorts of U2 . i) by A17, PBOOLE:def 18;
reconsider f' = F . i as Function of (the Sorts of U2 . i),(the Sorts of U3 . i) by A17, PBOOLE:def 18;
thus (F ** (h1 || FG)) . i = f' * h2' by A17, A28, MSUALG_3:2
.= (F ** (h2 || FG)) . i by A17, MSUALG_3:2 ; :: thesis:

end;

hence (F ** (h1 || FG)) . i = (F ** (h2 || FG)) . i ; :: thesis:

end;

then A29: F ** (h1 || FG) = F ** (h2 || FG) by PBOOLE:3;
A30: (F ** h1) || FG = F ** (h1 || FG) by Th8
.= (F ** h2) || FG by A29, Th8 ;
reconsider Fh1 = F ** h1, Fh2 = F ** h2 as ManySortedFunction of U1,U3 ;
( Fh1 is_homomorphism U1,U3 & Fh2 is_homomorphism U1,U3 ) by A1, A15, A16, MSUALG_3:10;
hence F ** h1 = F ** h2 by A30, Th18; :: thesis:

now

take i = j; :: thesis:
thus i in the carrier of S by A4; :: thesis:
A31: g = IFEQ i,j,g,((Reverse the Sorts of U2) . i) by FUNCOP_1:def 8
.= G . i by A4, A8 ;
A32: h = IFEQ i,j,h,((Reverse the Sorts of U2) . i) by FUNCOP_1:def 8
.= H . i by A4, A9 ;

now

let x be Element of FGj; :: thesis:
assume g = h ; :: thesis:
then g . x = x2 by FUNCOP_1:13;
hence contradiction by A6, FUNCOP_1:13; :: thesis:

end;

hence G <> H by A31, A32; :: thesis:

end;

hence h1 <> h2 by A15, A16; :: thesis:

end;

hence contradiction by A2; :: thesis: