let I be set ; :: thesis:
let A be ManySortedSet of I; :: thesis:
let B be non-empty ManySortedSet of I; :: thesis:
let F be ManySortedFunction of A,B; :: thesis:
assume A1: A is non-empty ; :: thesis:
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 ) :: thesis:

proof

assume A2: F is "1-1" ; :: thesis:
let C be ManySortedSet of I; :: thesis:
let G, H be ManySortedFunction of C,A; :: thesis:
assume A3: F ** G = F ** H ; :: thesis:

now :: thesis:

let i be object ; :: thesis:
assume A4: i in I ; :: thesis:
then 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; :: thesis:

end;

hence G = H ; :: thesis:

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" ; :: thesis:
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 H₁( 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 = H₁(i) from PBOOLE:sch 4();
take C ; :: thesis:
deffunc H₂( 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 = H₂(i) from PBOOLE:sch 4();
deffunc H₃( 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 = H₃(i) from PBOOLE:sch 4();

now :: thesis:

let G be ManySortedSet of I; :: thesis:
let g, h be Function of Z,(A . j); :: thesis:
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)) ; :: thesis:
thus G is Function-yielding :: thesis:

proof

let i be object ; :: according to FUNCOP_1:def 6 :: thesis:
assume i in dom G ; :: thesis:
then A17: i in I ;

now :: thesis:

per cases ;

case i = j ; :: thesis:

then IFEQ (i,j,g,((id C) . i)) = g by FUNCOP_1:def 8;
hence G . i is set by A16, A17; :: thesis:

end;

case i <> j ; :: thesis:

then IFEQ (i,j,g,((id C) . i)) = (id C) . i by FUNCOP_1:def 8;
hence G . i is set by A16, A17; :: thesis:

end;

hence G . i is set ; :: thesis:

end;

then reconsider G = G, H = H as ManySortedFunction of I by A11, A12, A14, A15;

now :: thesis:

let G be ManySortedFunction of I; :: thesis:
let g, h be Function of Z,(A . j); :: thesis:
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)) ; :: thesis:
thus G is ManySortedFunction of C,A :: thesis:

proof

let i be object ; :: according to PBOOLE:def 15 :: thesis:
assume A19: i in I ; :: thesis:

now :: thesis:

per cases ;

case A20: i = j ; :: thesis:

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; :: thesis:

end;

case A22: i <> j ; :: thesis:

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; :: thesis:

end;

hence G . i is Element of K19(K20((C . i),(A . i))) ; :: thesis:

end;

then reconsider G = G, H = H as ManySortedFunction of C,A by A11, A12, A14, A15;

A24: now :: thesis:

let i be object ; :: thesis:
assume A25: i in I ; :: thesis:

now :: thesis:

per cases ;

case A26: i = j ; :: thesis:

then 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 ;
:: thesis:

end;

case A28: i <> j ; :: thesis:

reconsider 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 ;
:: thesis:

end;

hence (F ** G) . i = (F ** H) . i ; :: thesis:

end;

take G ; :: thesis:
take H ; :: thesis:
( F ** G is ManySortedSet of I & F ** H is ManySortedSet of I ) by Lm1;
hence F ** G = F ** H by A24, PBOOLE:3; :: thesis:
ex i being set st
( i in I & G . i <> H . i )

proof

take i = j; :: thesis:
thus i in I by A8; :: thesis:
A30: h = IFEQ (i,j,h,((id C) . i)) by FUNCOP_1:def 8
.= H . i by A8, A15 ;
g = IFEQ (i,j,g,((id C) . i)) by FUNCOP_1:def 8
.= G . i by A8, A14 ;
hence G . i <> H . i by A12, A30; :: thesis:

end;

hence G <> H ; :: thesis:

end;

hence contradiction by A6; :: thesis: