let I be set ; :: thesis: for A being ManySortedSet of
for B being V2() ManySortedSet of
for F being ManySortedFunction of A,B holds
( F is "onto" iff for C being V2() ManySortedSet of
for G, H being ManySortedFunction of B,C st G ** F = H ** F holds
G = H )
let A be ManySortedSet of ; :: thesis: for B being V2() ManySortedSet of
for F being ManySortedFunction of A,B holds
( F is "onto" iff for C being V2() ManySortedSet of
for G, H being ManySortedFunction of B,C st G ** F = H ** F holds
G = H )
let B be V2() ManySortedSet of ; :: thesis: for F being ManySortedFunction of A,B holds
( F is "onto" iff for C being V2() ManySortedSet of
for G, H being ManySortedFunction of B,C st G ** F = H ** F holds
G = H )
let F be ManySortedFunction of A,B; :: thesis: ( F is "onto" iff for C being V2() ManySortedSet of
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
for G, H being ManySortedFunction of B,C st G ** F = H ** F holds
G = H ) :: thesis: ( ( for C being V2() ManySortedSet of
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" ; :: thesis: for C being V2() ManySortedSet of
for G, H being ManySortedFunction of B,C st G ** F = H ** F holds
G = H
let C be V2() ManySortedSet of ; :: thesis: for G, H being ManySortedFunction of B,C st G ** F = H ** F holds
G = H
let G, H be ManySortedFunction of B,C; :: thesis: ( G ** F = H ** F implies G = H )
assume A2: G ** F = H ** F ; :: thesis: G = H
now
let i be set ; :: thesis: ( i in I implies G . i = H . i )
assume A3: i in I ; :: thesis: G . i = H . i
then A4: ( B . i <> {} & C . i <> {} ) ;
reconsider f = F . i as Function of (A . i),(B . i) by A3, PBOOLE:def 18;
reconsider g = G . i as Function of (B . i),(C . i) by A3, PBOOLE:def 18;
reconsider h = H . i as Function of (B . i),(C . i) by A3, PBOOLE:def 18;
A5: rng f = B . i by A1, A3, MSUALG_3:def 3;
g * f = (H ** F) . i by A2, A3, MSUALG_3:2
.= h * f by A3, MSUALG_3:2 ;
hence G . i = H . i by A4, A5, FUNCT_2:22; :: thesis: verum
end;
hence G = H by PBOOLE:3; :: thesis: verum
end;
assume that
A6: for C being V2() ManySortedSet of
for G, H being ManySortedFunction of B,C st G ** F = H ** F holds
G = H and
A7: not F is "onto" ; :: thesis: contradiction
consider j being set such that
A8: ( j in I & rng (F . j) <> B . j ) by A7, MSUALG_3:def 3;
reconsider I = I as non empty set by A8;
reconsider j = j as Element of I by A8;
reconsider A = A, B = B as ManySortedSet of ;
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 <> {} & ex g, h being Function of (B . j),Z st
( g * f = h * f & g <> h ) ) by A8, FUNCT_2:22;
consider g, h being Function of (B . j),Z such that
A10: ( g * (F . j) = h * (F . j) & g <> h ) by A9;
ex C being ManySortedSet of st
( C is non-empty & ex G, H being ManySortedFunction of B,C st
( G ** F = H ** F & G <> H ) )
proof
deffunc H1( set ) -> set = IFEQ $1,j,Z,(B . $1);
consider C being ManySortedSet of such that
A11: for i being set st i in I holds
C . i = H1(i) from PBOOLE:sch 4();
 take C ; :: thesis: ( C is non-empty & ex G, H being ManySortedFunction of B,C st
( G ** F = H ** F & G <> H ) )
deffunc H2( set ) -> set = IFEQ $1,j,g,((id B) . $1);
consider G being ManySortedSet of such that
A12: for i being set st i in I holds
G . i = H2(i) from PBOOLE:sch 4();
 deffunc H3( set ) -> set = IFEQ $1,j,h,((id B) . $1);
consider H being ManySortedSet of such that
A13: for i being set st i in I holds
H . i = H3(i) from PBOOLE:sch 4();
 thus C is non-empty :: thesis: ex G, H being ManySortedFunction of B,C st
( G ** F = H ** F & G <> H )
proof
let i be set ; :: according to PBOOLE:def 16 :: thesis: ( not i in I or not C . i is empty )
assume A14: i in I ; :: thesis: not C . i is empty
now
per cases ( i = j or i <> j ) ;
case i = j ; :: thesis: not C . i is empty
then IFEQ i,j,Z,(B . i) = Z by FUNCOP_1:def 8;
hence not C . i is empty by A9, A11, A14; :: thesis: verum
end;
case i <> j ; :: thesis: not C . i is empty
then A15: IFEQ i,j,Z,(B . i) = B . i by FUNCOP_1:def 8;
thus not C . i is empty by A11, A14, A15; :: thesis: verum
end;
end;
end;
hence not C . i is empty ; :: thesis: verum
end;
now
let G be ManySortedSet of ; :: thesis: for g, h being Function of (B . j),Z st g * (F . j) = h * (F . j) & g <> h & ( for i being set 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; :: thesis: ( g * (F . j) = h * (F . j) & g <> h & ( for i being set 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) & g <> h ) and
A16: for i being set st i in I holds
G . i = IFEQ i,j,g,((id B) . i) ; :: thesis: G is Function-yielding
thus G is Function-yielding :: thesis: verum
proof
let i be set ; :: according to FUNCOP_1:def 6 :: thesis: ( not i in dom G or G . i is set )
assume i in dom G ; :: thesis: G . i is set
then A17: i in I by PARTFUN1:def 4;
now
per cases ( i = j or i <> j ) ;
case i = j ; :: thesis: G . i is set
then IFEQ i,j,g,((id B) . i) = g by FUNCOP_1:def 8;
hence G . i is set by A16, A17; :: thesis: verum
end;
case i <> j ; :: thesis: G . i is set
then IFEQ i,j,g,((id B) . i) = (id B) . i by FUNCOP_1:def 8;
hence G . i is set by A16, A17; :: thesis: verum
end;
end;
end;
hence G . i is set ; :: thesis: verum
end;
end;
then reconsider G = G, H = H as ManySortedFunction of by A10, A12, A13;
now
let G be ManySortedFunction of ; :: thesis: for g, h being Function of (B . j),Z st g * (F . j) = h * (F . j) & g <> h & ( for i being set st i in I holds
G . i = IFEQ i,j,g,((id B) . i) ) holds
G is ManySortedFunction of B,C
let g, h be Function of (B . j),Z; :: thesis: ( g * (F . j) = h * (F . j) & g <> h & ( for i being set 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) & g <> h ) and
A18: for i being set st i in I holds
G . i = IFEQ i,j,g,((id B) . i) ; :: thesis: G is ManySortedFunction of B,C
thus G is ManySortedFunction of B,C :: thesis: verum
proof
let i be set ; :: according to PBOOLE:def 18 :: thesis: ( not i in I or G . i is Element of K21(K22((B . i),(C . i))) )
assume A19: i in I ; :: thesis: G . i is Element of K21(K22((B . i),(C . i)))
now
per cases ( i = j or i <> j ) ;
case A20: i = j ; :: thesis: G . i is Element of K21(K22((B . i),(C . i)))
then A21: IFEQ i,j,g,((id B) . i) = g by FUNCOP_1:def 8;
A22: C . i = IFEQ i,j,Z,(B . i) by A11, A20;
IFEQ i,j,Z,(B . i) = Z by A20, FUNCOP_1:def 8;
hence G . i is Element of K21(K22((B . i),(C . i))) by A18, A20, A21, A22; :: thesis: verum
end;
case A23: i <> j ; :: thesis: G . i is Element of K21(K22((B . i),(C . i)))
then IFEQ i,j,g,((id B) . i) = (id B) . i by FUNCOP_1:def 8;
then A24: G . i = (id B) . i by A18, A19;
IFEQ i,j,Z,(B . i) = B . i by A23, FUNCOP_1:def 8;
then B . i = C . i by A11, A19;
hence G . i is Element of K21(K22((B . i),(C . i))) by A19, A24, PBOOLE:def 18; :: thesis: verum
end;
end;
end;
hence G . i is Element of K21(K22((B . i),(C . i))) ; :: thesis: verum
end;
end;
then reconsider G = G, H = H as ManySortedFunction of B,C by A10, A12, A13;
take G ; :: thesis: ex H being ManySortedFunction of B,C st
( G ** F = H ** F & G <> H )
take H ; :: thesis: ( G ** F = H ** F & G <> H )
A25: ( G ** F is ManySortedSet of & H ** F is ManySortedSet of ) by Lm1;
now
let i be set ; :: thesis: ( i in I implies (G ** F) . i = (H ** F) . i )
assume A26: i in I ; :: thesis: (G ** F) . i = (H ** F) . i
now
per cases ( i = j or i <> j ) ;
case A27: i = j ; :: thesis: (G ** F) . i = (H ** F) . i
then IFEQ i,j,g,((id B) . i) = g by FUNCOP_1:def 8;
then A28: g = G . i by A12, A26;
IFEQ i,j,h,((id B) . i) = h by A27, FUNCOP_1:def 8;
then A29: h = H . i by A13, A26;
thus (G ** F) . i = h * (F . j) by A10, A27, A28, MSUALG_3:2
.= (H ** F) . i by A27, A29, MSUALG_3:2 ; :: thesis: verum
end;
case A30: i <> j ; :: thesis: (G ** F) . i = (H ** F) . i
then A31: IFEQ i,j,g,((id B) . i) = (id B) . i by FUNCOP_1:def 8;
A32: IFEQ i,j,h,((id B) . i) = (id B) . i by A30, FUNCOP_1:def 8;
reconsider f' = F . i as Function of (A . i),(B . i) by A26, PBOOLE:def 18;
reconsider g' = G . i as Function of (B . i),(C . i) by A26, PBOOLE:def 18;
reconsider h' = H . i as Function of (B . i),(C . i) by A26, PBOOLE:def 18;
g' = (id B) . i by A12, A26, A31
.= h' by A13, A26, A32 ;
hence (G ** F) . i = h' * f' by A26, MSUALG_3:2
.= (H ** F) . i by A26, MSUALG_3:2 ;
:: thesis: verum
end;
end;
end;
hence (G ** F) . i = (H ** F) . i ; :: thesis: verum
end;
hence G ** F = H ** F by A25, PBOOLE:3; :: thesis: G <> H
ex i being set st
( i in I & G . i <> H . i )
proof
take i = j; :: thesis: ( i in I & G . i <> H . i )
thus i in I ; :: thesis: G . i <> H . i
A33: g = IFEQ i,j,g,((id B) . i) by FUNCOP_1:def 8
.= G . i by A12 ;
h = IFEQ i,j,h,((id B) . i) by FUNCOP_1:def 8
.= H . i by A13 ;
hence G . i <> H . i by A10, A33; :: thesis: verum
end;
hence G <> H ; :: thesis: verum
end;
hence contradiction by A6; :: thesis: verum