let I be set ; for A being ManySortedSet of I
for B being V2() ManySortedSet of I
for F being ManySortedFunction of A,B st A is V2() holds
( F is "1-1" iff for C being ManySortedSet of I
for G, H being ManySortedFunction of C,A st F ** G = F ** H holds
G = H )
let A be ManySortedSet of I; for B being V2() ManySortedSet of I
for F being ManySortedFunction of A,B st A is V2() holds
( F is "1-1" iff for C being ManySortedSet of I
for G, H being ManySortedFunction of C,A st F ** G = F ** H holds
G = H )
let B be V2() ManySortedSet of I; for F being ManySortedFunction of A,B st A is V2() holds
( F is "1-1" iff for C being ManySortedSet of I
for G, H being ManySortedFunction of C,A st F ** G = F ** H holds
G = H )
let F be ManySortedFunction of A,B; ( A is V2() implies ( F is "1-1" iff for C being ManySortedSet of I
for G, H being ManySortedFunction of C,A st F ** G = F ** H holds
G = H ) )
assume A1:
A is V2()
; ( F is "1-1" iff for C being ManySortedSet of I
for G, H being ManySortedFunction of C,A st F ** G = F ** H holds
G = H )
thus
( F is "1-1" implies for C being ManySortedSet of I
for G, H being ManySortedFunction of C,A st F ** G = F ** H holds
G = H )
( ( for C being ManySortedSet of I
for G, H being ManySortedFunction of C,A st F ** G = F ** H holds
G = H ) implies F is "1-1" )proof
assume A2:
F is
"1-1"
;
for C being ManySortedSet of I
for G, H being ManySortedFunction of C,A st F ** G = F ** H holds
G = H
let C be
ManySortedSet of
I;
for G, H being ManySortedFunction of C,A st F ** G = F ** H holds
G = Hlet G,
H be
ManySortedFunction of
C,
A;
( F ** G = F ** H implies G = H )
assume A3:
F ** G = F ** H
;
G = H
now for i being object st i in I holds
G . i = H . ilet i be
object ;
( i in I implies G . i = H . i )assume A4:
i in I
;
G . i = H . ithen reconsider f =
F . i as
Function of
(A . i),
(B . i) by PBOOLE:def 15;
reconsider h =
H . i as
Function of
(C . i),
(A . i) by A4, PBOOLE:def 15;
reconsider g =
G . i as
Function of
(C . i),
(A . i) by A4, PBOOLE:def 15;
A5:
f is
one-to-one
by A2, A4, MSUALG_3:1;
f * g =
(F ** H) . i
by A3, A4, MSUALG_3:2
.=
f * h
by A4, MSUALG_3:2
;
hence
G . i = H . i
by A1, A4, A5, FUNCT_2:21;
verum end;
hence
G = H
;
verum
end;
assume that
A6:
for C being ManySortedSet of I
for G, H being ManySortedFunction of C,A st F ** G = F ** H holds
G = H
and
A7:
not F is "1-1"
; contradiction
consider j being set such that
A8:
j in I
and
A9:
not F . j is one-to-one
by A7, MSUALG_3:1;
F . j is Function of (A . j),(B . j)
by A8, PBOOLE:def 15;
then consider Z being set such that
A10:
ex g, h being Function of Z,(A . j) st
( (F . j) * g = (F . j) * h & g <> h )
by A1, A8, A9, FUNCT_2:21;
consider g, h being Function of Z,(A . j) such that
A11:
(F . j) * g = (F . j) * h
and
A12:
g <> h
by A10;
ex C being ManySortedSet of I ex G, H being ManySortedFunction of C,A st
( F ** G = F ** H & G <> H )
proof
deffunc H1(
object )
-> set =
IFEQ ($1,
j,
Z,
(A . $1));
consider C being
ManySortedSet of
I such that A13:
for
i being
object st
i in I holds
C . i = H1(
i)
from PBOOLE:sch 4();
take
C
;
ex G, H being ManySortedFunction of C,A st
( F ** G = F ** H & G <> H )
deffunc H2(
object )
-> set =
IFEQ ($1,
j,
g,
((id C) . $1));
consider G being
ManySortedSet of
I such that A14:
for
i being
object st
i in I holds
G . i = H2(
i)
from PBOOLE:sch 4();
deffunc H3(
object )
-> set =
IFEQ ($1,
j,
h,
((id C) . $1));
consider H being
ManySortedSet of
I such that A15:
for
i being
object st
i in I holds
H . i = H3(
i)
from PBOOLE:sch 4();
now for G being ManySortedSet of I
for g, h being Function of Z,(A . j) st (F . j) * g = (F . j) * h & g <> h & ( for i being object st i in I holds
G . i = IFEQ (i,j,g,((id C) . i)) ) holds
G is Function-yielding let G be
ManySortedSet of
I;
for g, h being Function of Z,(A . j) st (F . j) * g = (F . j) * h & g <> h & ( for i being object st i in I holds
G . i = IFEQ (i,j,g,((id C) . i)) ) holds
G is Function-yielding let g,
h be
Function of
Z,
(A . j);
( (F . j) * g = (F . j) * h & g <> h & ( for i being object st i in I holds
G . i = IFEQ (i,j,g,((id C) . i)) ) implies G is Function-yielding )assume that
(F . j) * g = (F . j) * h
and
g <> h
and A16:
for
i being
object st
i in I holds
G . i = IFEQ (
i,
j,
g,
((id C) . i))
;
G is Function-yielding thus
G is
Function-yielding
verum end;
then reconsider G =
G,
H =
H as
ManySortedFunction of
I by A11, A12, A14, A15;
now for G being ManySortedFunction of I
for g, h being Function of Z,(A . j) st (F . j) * g = (F . j) * h & g <> h & ( for i being object st i in I holds
G . i = IFEQ (i,j,g,((id C) . i)) ) holds
G is ManySortedFunction of C,Alet G be
ManySortedFunction of
I;
for g, h being Function of Z,(A . j) st (F . j) * g = (F . j) * h & g <> h & ( for i being object st i in I holds
G . i = IFEQ (i,j,g,((id C) . i)) ) holds
G is ManySortedFunction of C,Alet g,
h be
Function of
Z,
(A . j);
( (F . j) * g = (F . j) * h & g <> h & ( for i being object st i in I holds
G . i = IFEQ (i,j,g,((id C) . i)) ) implies G is ManySortedFunction of C,A )assume that
(F . j) * g = (F . j) * h
and
g <> h
and A18:
for
i being
object st
i in I holds
G . i = IFEQ (
i,
j,
g,
((id C) . i))
;
G is ManySortedFunction of C,Athus
G is
ManySortedFunction of
C,
A
verumproof
let i be
object ;
PBOOLE:def 15 ( not i in I or G . i is Element of K19(K20((C . i),(A . i))) )
assume A19:
i in I
;
G . i is Element of K19(K20((C . i),(A . i)))
now ( ( i = j & G . i is Element of K19(K20((C . i),(A . i))) ) or ( i <> j & G . i is Element of K19(K20((C . i),(A . i))) ) )per cases
( i = j or i <> j )
;
case A20:
i = j
;
G . i is Element of K19(K20((C . i),(A . i)))then A21:
(
IFEQ (
i,
j,
g,
((id C) . i))
= g &
IFEQ (
i,
j,
Z,
(A . i))
= Z )
by FUNCOP_1:def 8;
C . i = IFEQ (
i,
j,
Z,
(A . i))
by A13, A19;
hence
G . i is
Element of
K19(
K20(
(C . i),
(A . i)))
by A18, A19, A20, A21;
verum end; case A22:
i <> j
;
G . i is Element of K19(K20((C . i),(A . i)))then
IFEQ (
i,
j,
Z,
(A . i))
= A . i
by FUNCOP_1:def 8;
then A23:
C . i = A . i
by A13, A19;
IFEQ (
i,
j,
g,
((id C) . i))
= (id C) . i
by A22, FUNCOP_1:def 8;
then
G . i = (id C) . i
by A18, A19;
hence
G . i is
Element of
K19(
K20(
(C . i),
(A . i)))
by A19, A23, PBOOLE:def 15;
verum end; end; end;
hence
G . i is
Element of
K19(
K20(
(C . i),
(A . i)))
;
verum
end; end;
then reconsider G =
G,
H =
H as
ManySortedFunction of
C,
A by A11, A12, A14, A15;
A24:
now for i being object st i in I holds
(F ** G) . i = (F ** H) . ilet i be
object ;
( i in I implies (F ** G) . i = (F ** H) . i )assume A25:
i in I
;
(F ** G) . i = (F ** H) . inow ( ( i = j & (F ** G) . i = (F ** H) . i ) or ( i <> j & (F ** G) . i = (F ** H) . i ) )per cases
( i = j or i <> j )
;
case A26:
i = j
;
(F ** G) . i = (F ** H) . ithen
IFEQ (
i,
j,
h,
((id C) . i))
= h
by FUNCOP_1:def 8;
then A27:
h = H . i
by A15, A25;
IFEQ (
i,
j,
g,
((id C) . i))
= g
by A26, FUNCOP_1:def 8;
then
g = G . i
by A14, A25;
hence (F ** G) . i =
(F . j) * h
by A8, A11, A26, MSUALG_3:2
.=
(F ** H) . i
by A8, A26, A27, MSUALG_3:2
;
verum end; case A28:
i <> j
;
(F ** G) . i = (F ** H) . ireconsider g9 =
G . i as
Function of
(C . i),
(A . i) by A25, PBOOLE:def 15;
reconsider f9 =
F . i as
Function of
(A . i),
(B . i) by A25, PBOOLE:def 15;
reconsider h9 =
H . i as
Function of
(C . i),
(A . i) by A25, PBOOLE:def 15;
A29:
IFEQ (
i,
j,
h,
((id C) . i))
= (id C) . i
by A28, FUNCOP_1:def 8;
IFEQ (
i,
j,
g,
((id C) . i))
= (id C) . i
by A28, FUNCOP_1:def 8;
then g9 =
(id C) . i
by A14, A25
.=
h9
by A15, A25, A29
;
hence (F ** G) . i =
f9 * h9
by A25, MSUALG_3:2
.=
(F ** H) . i
by A25, MSUALG_3:2
;
verum end; end; end; hence
(F ** G) . i = (F ** H) . i
;
verum end;
take
G
;
ex H being ManySortedFunction of C,A st
( F ** G = F ** H & G <> H )
take
H
;
( F ** G = F ** H & G <> H )
(
F ** G is
ManySortedSet of
I &
F ** H is
ManySortedSet of
I )
by Lm1;
hence
F ** G = F ** H
by A24, PBOOLE:3;
G <> H
ex
i being
set st
(
i in I &
G . i <> H . i )
hence
G <> H
;
verum
end;
hence
contradiction
by A6; verum