let I be set ; :: thesis: for A being ManySortedSet of I
for B being non-empty ManySortedSet of I
for F being ManySortedFunction of A,B holds
( F is "onto" iff for C being non-empty 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; :: thesis: for B being non-empty ManySortedSet of I
for F being ManySortedFunction of A,B holds
( F is "onto" iff for C being non-empty ManySortedSet of I
for G, H being ManySortedFunction of B,C st G ** F = H ** F holds
G = H )
let B be non-empty ManySortedSet of I; :: thesis: for F being ManySortedFunction of A,B holds
( F is "onto" iff for C being non-empty 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; :: thesis: ( F is "onto" iff for C being non-empty 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 non-empty ManySortedSet of I
for G, H being ManySortedFunction of B,C st G ** F = H ** F holds
G = H ) :: thesis: ( ( for C being non-empty 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" ; :: thesis: for C being non-empty ManySortedSet of I
for G, H being ManySortedFunction of B,C st G ** F = H ** F holds
G = H
let C be non-empty ManySortedSet of I; :: 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 :: thesis: for i being object st i in I holds
G . i = H . i
let i be object ; :: thesis: ( i in I implies G . i = H . i )
assume A3: i in I ; :: thesis: G . i = H . i
then 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; :: thesis: verum
end;
hence G = H ; :: thesis: verum
end;
assume that
A5: for C being non-empty 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" ; :: thesis: 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 non-empty & 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 ; :: thesis: ( C is non-empty & ex G, H being ManySortedFunction of B,C st
( G ** F = H ** F & G <> H ) )
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 object ; :: according to PBOOLE:def 13 :: thesis: ( not i in I or not C . i is empty )
assume A14: i in I ; :: thesis: not C . i is empty
now :: thesis: ( ( i = j & not C . i is empty ) or ( i <> j & not C . i is empty ) )
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, A13, A14; :: thesis: verum
end;
case i <> j ; :: thesis: not C . i is empty
then IFEQ (i,j,Z,(B . i)) = B . i by FUNCOP_1:def 8;
hence not C . i is empty by A13, A14; :: thesis: verum
end;
end;
end;
hence not C . i is empty ; :: thesis: verum
end;
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 :: thesis: 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; :: thesis: 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; :: thesis: ( 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)) ; :: thesis: G is Function-yielding
thus G is Function-yielding :: thesis: verum
proof
let i be object ; :: 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 A18: i in I ;
now :: thesis: ( ( i = j & G . i is set ) or ( i <> j & G . i is set ) )
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 A17, A18; :: 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 A17, A18; :: thesis: verum
end;
end;
end;
hence G . i is set ; :: thesis: verum
end;
end;
then reconsider G = G, H = H as ManySortedFunction of I by A11, A12, A15, A16;
now :: thesis: 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,C
let G be ManySortedFunction of I; :: thesis: 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,C
let g, h be Function of (B . j),Z; :: thesis: ( 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)) ; :: thesis: G is ManySortedFunction of B,C
thus G is ManySortedFunction of B,C :: thesis: verum
proof
let i be object ; :: according to PBOOLE:def 15 :: thesis: ( not i in I or G . i is Element of K19(K20((B . i),(C . i))) )
assume A20: i in I ; :: thesis: G . i is Element of K19(K20((B . i),(C . i)))
now :: thesis: ( ( 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 ; :: thesis: 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; :: thesis: verum
end;
case A23: i <> j ; :: thesis: 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; :: thesis: verum
end;
end;
end;
hence G . i is Element of K19(K20((B . i),(C . i))) ; :: thesis: verum
end;
end;
then reconsider G = G, H = H as ManySortedFunction of B,C by A11, A12, A15, A16;
A25: now :: thesis: for i being object st i in I holds
(G ** F) . i = (H ** F) . i
let i be object ; :: thesis: ( i in I implies (G ** F) . i = (H ** F) . i )
assume A26: i in I ; :: thesis: (G ** F) . i = (H ** F) . i
now :: thesis: ( ( 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 ; :: thesis: (G ** F) . i = (H ** F) . i
then 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 ;
:: thesis: verum
end;
case A29: i <> j ; :: thesis: (G ** F) . i = (H ** F) . i
reconsider 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 ;
:: thesis: verum
end;
end;
end;
hence (G ** F) . i = (H ** F) . i ; :: thesis: verum
end;
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 )
( G ** F is ManySortedSet of I & H ** F is ManySortedSet of I ) by Lm1;
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
A31: h = IFEQ (i,j,h,((id B) . i)) by FUNCOP_1:def 8
.= H . i by A16 ;
g = IFEQ (i,j,g,((id B) . i)) by FUNCOP_1:def 8
.= G . i by A15 ;
hence G . i <> H . i by A12, A31; :: thesis: verum
end;
hence G <> H ; :: thesis: verum
end;
hence contradiction by A5; :: thesis: verum