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

let i be set ; :: thesis:
assume A4: i in I ; :: thesis:
then A5: ( A . i <> {} & B . i <> {} ) by A1;
reconsider f = F . i as Function of A . i,B . i by A4, PBOOLE:def 18;
reconsider g = G . i as Function of C . i,A . i by A4, PBOOLE:def 18;
reconsider h = H . i as Function of C . i,A . i by A4, PBOOLE:def 18;
A6: 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 A5, A6, FUNCT_2:27; :: thesis:

end;

hence G = H by PBOOLE:3; :: thesis:

end;

assume that
A7: for C being ManySortedSet of I
for G, H being ManySortedFunction of C,A st F ** G = F ** H holds
G = H and
A8: not F is "1-1" ; :: thesis:
consider j being set such that
A9: ( j in I & not F . j is one-to-one ) by A8, MSUALG_3:1;
A10: ( A . j <> {} & B . j <> {} ) by A1, A9;
F . j is Function of A . j,B . j by A9, PBOOLE:def 18;
then consider Z being set such that
A11: ex g, h being Function of Z,A . j st
( (F . j) * g = (F . j) * h & g <> h ) by A9, A10, FUNCT_2:27;
consider g, h being Function of Z,A . j such that
A12: ( (F . j) * g = (F . j) * h & g <> h ) by A11;
ex C being ManySortedSet of I ex G, H being ManySortedFunction of C,A st
( F ** G = F ** H & G <> H )

proof

deffunc H₁( set ) -> set = IFEQ $1,j,Z,(A . $1);
consider C being ManySortedSet of I such that
A13: for i being set st i in I holds
C . i = H₁(i) from PBOOLE:sch 4();
take C ; :: thesis:
deffunc H₂( set ) -> set = IFEQ $1,j,g,((id C) . $1);
consider G being ManySortedSet of I such that
A14: for i being set st i in I holds
G . i = H₂(i) from PBOOLE:sch 4();
deffunc H₃( set ) -> set = IFEQ $1,j,h,((id C) . $1);
consider H being ManySortedSet of I such that
A15: for i being set st i in I holds
H . i = H₃(i) from PBOOLE:sch 4();

now

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 & g <> h ) and
A16: for i being set 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 set ; :: according to FUNCOP_1:def 6 :: thesis:
assume i in dom G ; :: thesis:
then A17: i in I by PBOOLE:def 3;

now

per cases ;

case i = j ; :: thesis:

then IFEQ i,j,g,((id C) . i) = g by FUNCOP_1:def 8;
hence G . i is Function 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 Function by A16, A17; :: thesis:

end;

hence G . i is Function ; :: thesis:

end;

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

now

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 & g <> h ) and
A18: for i being set 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 set ; :: according to PBOOLE:def 18 :: thesis:
assume A19: i in I ; :: thesis:

now

per cases ;

case A20: i = j ; :: thesis:

then A21: IFEQ i,j,g,((id C) . i) = g by FUNCOP_1:def 8;
A22: C . i = IFEQ i,j,Z,(A . i) by A13, A19;
IFEQ i,j,Z,(A . i) = Z by A20, FUNCOP_1:def 8;
hence G . i is Function of C . i,A . i by A18, A19, A20, A21, A22; :: thesis:

end;

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

then IFEQ i,j,g,((id C) . i) = (id C) . i by FUNCOP_1:def 8;
then A24: G . i = (id C) . i by A18, A19;
IFEQ i,j,Z,(A . i) = A . i by A23, FUNCOP_1:def 8;
then C . i = A . i by A13, A19;
hence G . i is Function of C . i,A . i by A19, A24, PBOOLE:def 18; :: thesis:

end;

hence G . i is Function of C . i,A . i ; :: thesis:

end;

then reconsider G = G, H = H as ManySortedFunction of C,A by A12, A14, A15;
take G ; :: thesis:
take H ; :: thesis:
A25: ( F ** G is ManySortedSet of I & F ** H is ManySortedSet of I ) by Lm1;

now

let i be set ; :: thesis:
assume A26: i in I ; :: thesis:

now

per cases ;

case A27: i = j ; :: thesis:

then IFEQ i,j,g,((id C) . i) = g by FUNCOP_1:def 8;
then A28: g = G . i by A14, A26;
IFEQ i,j,h,((id C) . i) = h by A27, FUNCOP_1:def 8;
then A29: h = H . i by A15, A26;
thus (F ** G) . i = (F . j) * h by A9, A12, A27, A28, MSUALG_3:2
.= (F ** H) . i by A9, A27, A29, MSUALG_3:2 ; :: thesis:

end;

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

then A31: IFEQ i,j,g,((id C) . i) = (id C) . i by FUNCOP_1:def 8;
A32: IFEQ i,j,h,((id C) . i) = (id C) . 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 C . i,A . i by A26, PBOOLE:def 18;
reconsider h' = H . i as Function of C . i,A . i by A26, PBOOLE:def 18;
g' = (id C) . i by A14, A26, A31
.= h' by A15, A26, A32 ;
hence (F ** G) . i = f' * h' by A26, MSUALG_3:2
.= (F ** H) . i by A26, MSUALG_3:2 ;
:: thesis:

end;

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

end;

hence F ** G = F ** H by A25, 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 A9; :: thesis:
A33: g = IFEQ i,j,g,((id C) . i) by FUNCOP_1:def 8
.= G . i by A9, A14 ;
h = IFEQ i,j,h,((id C) . i) by FUNCOP_1:def 8
.= H . i by A9, A15 ;
hence G . i <> H . i by A12, A33; :: thesis:

end;

hence G <> H ; :: thesis:

end;

hence contradiction by A7; :: thesis: