let S be non empty non void ManySortedSign ; :: thesis:
let U2, U3 be non-empty MSAlgebra over S; :: thesis:
let F be ManySortedFunction of U2,U3; :: thesis:
assume A1: F is_homomorphism U2,U3 ; :: thesis:
set C = the Sorts of U3;
set B = the Sorts of U2;
thus ( F is_monomorphism U2,U3 implies for U1 being non-empty MSAlgebra over 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 Th13; :: thesis:
set I = the carrier of S;
assume that
A2: for U1 being non-empty MSAlgebra over 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:
not F is "1-1" by A1, A3;
then consider j being set such that
A4: j in the carrier of S and
A5: not F . j is one-to-one by MSUALG_3:1;
set f = F . j;
F . j is Function of ( the Sorts of U2 . j),( the Sorts of U3 . j) by A4, PBOOLE:def 15;
then consider x1, x2 being object such that
A6: x1 in the Sorts of U2 . j and
A7: x2 in the Sorts of U2 . j and
A8: (F . j) . x1 = (F . j) . x2 and
A9: x1 <> x2 by A4, A5, FUNCT_2:19;
ex U1 being non-empty MSAlgebra over 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 ;
FG is non-empty by MSAFREE:14;
then reconsider FGj = FG . j, Bj = the Sorts of U2 . j as non empty set by A4;
reconsider h = FGj --> x2 as Function of FGj,Bj by A7, FUNCOP_1:45;
reconsider g = FGj --> x1 as Function of FGj,Bj by A6, FUNCOP_1:45;
set r = Reverse the Sorts of U2;
deffunc H₁( object ) -> set = IFEQ ($1,j,g,((Reverse the Sorts of U2) . $1));
consider G being ManySortedSet of the carrier of S such that
A10: for i being object st i in the carrier of S holds
G . i = H₁(i) from PBOOLE:sch 4();
deffunc H₂( object ) -> set = IFEQ ($1,j,h,((Reverse the Sorts of U2) . $1));
consider H being ManySortedSet of the carrier of S such that
A11: for i being object st i in the carrier of S holds
H . i = H₂(i) from PBOOLE:sch 4();

now :: thesis:

let G be ManySortedSet of the carrier of S; :: thesis:
let g, h be Function of FGj,Bj; :: thesis:
assume A12: for i being object 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 object ; :: according to FUNCOP_1:def 6 :: thesis:
assume i in dom G ; :: thesis:
then A13: i in the carrier of S ;

now :: thesis:

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 A12, A13; :: 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 A12, A13; :: thesis:

end;

hence G . i is set ; :: thesis:

end;

then reconsider G = G, H = H as ManySortedFunction of the carrier of S by A10, A11;

now :: thesis:

let G be ManySortedFunction of the carrier of S; :: thesis:
let g, h be Function of FGj,Bj; :: thesis:
assume A14: for i being object 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 object ; :: according to PBOOLE:def 15 :: thesis:
assume A15: i in the carrier of S ; :: thesis:

now :: thesis:

per cases ;

case A16: 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 K19(K20((FG . i),( the Sorts of U2 . i))) by A14, A15, A16; :: 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 A14, A15;
hence G . i is Element of K19(K20((FG . i),( the Sorts of U2 . i))) by A15, PBOOLE:def 15; :: thesis:

end;

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

end;

then reconsider G = G, H = H as ManySortedFunction of FG, the Sorts of U2 by A10, A11;
A17: FG is free by MSAFREE:16;
then consider h1 being ManySortedFunction of U1,U2 such that
A18: h1 is_homomorphism U1,U2 and
A19: h1 || FG = G by MSAFREE:def 5;
consider h2 being ManySortedFunction of U1,U2 such that
A20: h2 is_homomorphism U1,U2 and
A21: h2 || FG = H by A17, MSAFREE:def 5;
take h1 ; :: thesis:
take h2 ; :: thesis:
thus ( h1 is_homomorphism U1,U2 & h2 is_homomorphism U1,U2 ) by A18, A20; :: thesis:
reconsider Fh1 = F ** h1, Fh2 = F ** h2 as ManySortedFunction of U1,U3 ;
A22: Fh1 is_homomorphism U1,U3 by A1, A18, MSUALG_3:10;

now :: thesis:

let i be object ; :: thesis:
assume A23: i in the carrier of S ; :: thesis:

now :: thesis:

per cases ;

case A24: i = j ; :: thesis:

then A25: F . j is Function of ( the Sorts of U2 . i),( the Sorts of U3 . i) by A4, PBOOLE:def 15;
then reconsider fg = (F . j) * g as Function of FGj,( the Sorts of U3 . i) by A24, FUNCT_2:13;
reconsider fh = (F . j) * h as Function of FGj,( the Sorts of U3 . i) by A24, A25, FUNCT_2:13;

now :: thesis:

let x be object ; :: thesis:
assume A26: x in FGj ; :: thesis:
hence fg . x = (F . j) . (g . x) by FUNCT_2:15
.= (F . j) . x2 by A8, A26, FUNCOP_1:7
.= (F . j) . (h . x) by A26, FUNCOP_1:7
.= fh . x by A26, FUNCT_2:15 ;
:: thesis:

end;

then A27: (F . j) * g = (F . j) * h by FUNCT_2:12;
IFEQ (i,j,g,((Reverse the Sorts of U2) . i)) = g by A24, FUNCOP_1:def 8;
then g = (h1 || FG) . i by A10, A19, A23;
then A28: (F ** (h1 || FG)) . i = (F . j) * g by A4, A24, MSUALG_3:2;
IFEQ (i,j,h,((Reverse the Sorts of U2) . i)) = h by A24, FUNCOP_1:def 8;
then h = (h2 || FG) . i by A11, A21, A23;
hence (F ** (h1 || FG)) . i = (F ** (h2 || FG)) . i by A4, A24, A27, A28, MSUALG_3:2; :: thesis:

end;

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

reconsider f9 = F . i as Function of ( the Sorts of U2 . i),( the Sorts of U3 . i) by A23, PBOOLE:def 15;
reconsider h29 = (h2 || FG) . i as Function of (FG . i),( the Sorts of U2 . i) by A23, PBOOLE:def 15;
A30: IFEQ (i,j,h,((Reverse the Sorts of U2) . i)) = (Reverse the Sorts of U2) . i by A29, FUNCOP_1:def 8;
IFEQ (i,j,g,((Reverse the Sorts of U2) . i)) = (Reverse the Sorts of U2) . i by A29, FUNCOP_1:def 8;
then (h1 || FG) . i = (Reverse the Sorts of U2) . i by A10, A19, A23
.= (h2 || FG) . i by A11, A21, A23, A30 ;
hence (F ** (h1 || FG)) . i = f9 * h29 by A23, MSUALG_3:2
.= (F ** (h2 || FG)) . i by A23, MSUALG_3:2 ;
:: thesis:

end;

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

end;

then A31: F ** (h1 || FG) = F ** (h2 || FG) ;
A32: Fh2 is_homomorphism U1,U3 by A1, A20, MSUALG_3:10;
(F ** h1) || FG = F ** (h1 || FG) by Th4
.= (F ** h2) || FG by A31, Th4 ;
hence F ** h1 = F ** h2 by A22, A32, Th14; :: thesis:

now :: thesis:

take i = j; :: thesis:
thus i in the carrier of S by A4; :: thesis:

A33: now :: thesis:

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

end;

A34: h = IFEQ (i,j,h,((Reverse the Sorts of U2) . i)) by FUNCOP_1:def 8
.= H . i by A4, A11 ;
g = IFEQ (i,j,g,((Reverse the Sorts of U2) . i)) by FUNCOP_1:def 8
.= G . i by A4, A10 ;
hence G <> H by A34, A33; :: thesis:

end;

hence h1 <> h2 by A19, A21; :: thesis:

end;

hence contradiction by A2; :: thesis: