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