let X, Y be ManySortedSet of I; :: thesis: ( ( for i being object st i in I holds
ex F being Function of (A . i),(Union (coprod A)) st
( X . i = F & ( for x being object st x in A . i holds
F . x = [x,i] ) ) ) & ( for i being object st i in I holds
ex F being Function of (A . i),(Union (coprod A)) st
( Y . i = F & ( for x being object st x in A . i holds
F . x = [x,i] ) ) ) implies X = Y )
assume that
A7: for i being object st i in I holds
ex F being Function of (A . i),(Union (coprod A)) st
( X . i = F & ( for x being object st x in A . i holds
F . x = [x,i] ) ) and
A8: for i being object st i in I holds
ex F being Function of (A . i),(Union (coprod A)) st
( Y . i = F & ( for x being object st x in A . i holds
F . x = [x,i] ) ) ; :: thesis: X = Y
let i be object ; :: according to PBOOLE:def 10 :: thesis: ( not i in I or X . i = Y . i )
assume A9: i in I ; :: thesis: X . i = Y . i
consider F being Function of (A . i),(Union (coprod A)) such that
A10: X . i = F and
A11: for x being object st x in A . i holds
F . x = [x,i] by A7, A9;
consider G being Function of (A . i),(Union (coprod A)) such that
A12: Y . i = G and
A13: for x being object st x in A . i holds
G . x = [x,i] by A8, A9;
per cases ( A . i is empty or not A . i is empty ) ;
suppose A . i is empty ; :: thesis: X . i = Y . i
then ( G = {} & F = {} ) ;
hence X . i = Y . i by A10, A12; :: thesis: verum
end;
suppose A14: not A . i is empty ; :: thesis: X . i = Y . i
F = G
proof
let x be Element of A . i; :: according to FUNCT_2:def 8 :: thesis: F . x = G . x
thus F . x = [x,i] by A11, A14
.= G . x by A13, A14 ; :: thesis: verum
end;
hence X . i = Y . i by A10, A12; :: thesis: verum
end;
end;