let S be non empty non void ManySortedSign ; for U2, U3 being non-empty MSAlgebra over S
for F being ManySortedFunction of U2,U3 st F is_homomorphism U2,U3 holds
( F is_monomorphism U2,U3 iff 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 )
let U2, U3 be non-empty MSAlgebra over S; for F being ManySortedFunction of U2,U3 st F is_homomorphism U2,U3 holds
( F is_monomorphism U2,U3 iff 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 )
let F be ManySortedFunction of U2,U3; ( F is_homomorphism U2,U3 implies ( F is_monomorphism U2,U3 iff 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 ) )
assume A1:
F is_homomorphism U2,U3
; ( F is_monomorphism U2,U3 iff 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 )
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; ( ( 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 ) implies F is_monomorphism U2,U3 )
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
; contradiction
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;
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 )
reconsider FG =
FreeGen the
Sorts of
U2 as
GeneratorSet of
U1 ;
FG is
V2()
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 H1(
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 = H1(
i)
from PBOOLE:sch 4();
deffunc H2(
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 = H2(
i)
from PBOOLE:sch 4();
now for G being ManySortedSet of the carrier of S
for g, h being Function of FGj,Bj st ( for i being object st i in the carrier of S holds
G . i = IFEQ (i,j,g,((Reverse the Sorts of U2) . i)) ) holds
G is Function-yielding let G be
ManySortedSet of the
carrier of
S;
for g, h being Function of FGj,Bj st ( for i being object st i in the carrier of S holds
G . i = IFEQ (i,j,g,((Reverse the Sorts of U2) . i)) ) holds
G is Function-yielding let g,
h be
Function of
FGj,
Bj;
( ( for i being object st i in the carrier of S holds
G . i = IFEQ (i,j,g,((Reverse the Sorts of U2) . i)) ) implies G is Function-yielding )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))
;
G is Function-yielding thus
G is
Function-yielding
verum end;
then reconsider G =
G,
H =
H as
ManySortedFunction of the
carrier of
S by A10, A11;
now for G being ManySortedFunction of the carrier of S
for g, h being Function of FGj,Bj st ( for i being object st i in the carrier of S holds
G . i = IFEQ (i,j,g,((Reverse the Sorts of U2) . i)) ) holds
G is ManySortedFunction of FG, the Sorts of U2let G be
ManySortedFunction of the
carrier of
S;
for g, h being Function of FGj,Bj st ( for i being object st i in the carrier of S holds
G . i = IFEQ (i,j,g,((Reverse the Sorts of U2) . i)) ) holds
G is ManySortedFunction of FG, the Sorts of U2let g,
h be
Function of
FGj,
Bj;
( ( for i being object st i in the carrier of S holds
G . i = IFEQ (i,j,g,((Reverse the Sorts of U2) . i)) ) implies G is ManySortedFunction of FG, the Sorts of U2 )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))
;
G is ManySortedFunction of FG, the Sorts of U2thus
G is
ManySortedFunction of
FG, the
Sorts of
U2
verum 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
;
ex 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 )
take
h2
;
( h1 is_homomorphism U1,U2 & h2 is_homomorphism U1,U2 & F ** h1 = F ** h2 & h1 <> h2 )
thus
(
h1 is_homomorphism U1,
U2 &
h2 is_homomorphism U1,
U2 )
by A18, A20;
( F ** h1 = F ** h2 & h1 <> h2 )
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 for i being object st i in the carrier of S holds
(F ** (h1 || FG)) . i = (F ** (h2 || FG)) . ilet i be
object ;
( i in the carrier of S implies (F ** (h1 || FG)) . i = (F ** (h2 || FG)) . i )assume A23:
i in the
carrier of
S
;
(F ** (h1 || FG)) . i = (F ** (h2 || FG)) . inow ( ( i = j & (F ** (h1 || FG)) . i = (F ** (h2 || FG)) . i ) or ( i <> j & (F ** (h1 || FG)) . i = (F ** (h2 || FG)) . i ) )per cases
( i = j or i <> j )
;
case A24:
i = j
;
(F ** (h1 || FG)) . i = (F ** (h2 || FG)) . ithen 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;
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;
verum end; case A29:
i <> j
;
(F ** (h1 || FG)) . i = (F ** (h2 || FG)) . ireconsider 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
;
verum end; end; end; hence
(F ** (h1 || FG)) . i = (F ** (h2 || FG)) . i
;
verum 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;
h1 <> h2
hence
h1 <> h2
by A19, A21;
verum
end;
hence
contradiction
by A2; verum