let I be set ; :: thesis: for F, D, R being ManySortedSet of I st ( for i being object st i in I holds
ex f being Function st
( f = F . i & dom f = D . i & rng f = R . i ) ) & ( for i, j being object
for f, g being Function st i in I & j in I & i <> j & f = F . i & g = F . j holds
dom f misses dom g ) holds
ex G being Function st
( G = union (rng F) & dom G = union (rng D) & rng G = union (rng R) & ( for i, x being object
for f being Function st i in I & f = F . i & x in dom f holds
G . x = f . x ) )
let F, D, R be ManySortedSet of I; :: thesis: ( ( for i being object st i in I holds
ex f being Function st
( f = F . i & dom f = D . i & rng f = R . i ) ) & ( for i, j being object
for f, g being Function st i in I & j in I & i <> j & f = F . i & g = F . j holds
dom f misses dom g ) implies ex G being Function st
( G = union (rng F) & dom G = union (rng D) & rng G = union (rng R) & ( for i, x being object
for f being Function st i in I & f = F . i & x in dom f holds
G . x = f . x ) ) )
assume A1: for i being object st i in I holds
ex f being Function st
( f = F . i & dom f = D . i & rng f = R . i ) ; :: thesis: ( ex i, j being object ex f, g being Function st
( i in I & j in I & i <> j & f = F . i & g = F . j & not dom f misses dom g ) or ex G being Function st
( G = union (rng F) & dom G = union (rng D) & rng G = union (rng R) & ( for i, x being object
for f being Function st i in I & f = F . i & x in dom f holds
G . x = f . x ) ) )
assume A2: for i, j being object
for f, g being Function st i in I & j in I & i <> j & f = F . i & g = F . j holds
dom f misses dom g ; :: thesis: ex G being Function st
( G = union (rng F) & dom G = union (rng D) & rng G = union (rng R) & ( for i, x being object
for f being Function st i in I & f = F . i & x in dom f holds
G . x = f . x ) )
P0: dom F = I by PARTFUN1:def 2;
R0: dom R = I by PARTFUN1:def 2;
Q0: dom D = I by PARTFUN1:def 2;
P1: for z being object st z in union (rng F) holds
ex x, y, i being object st
( z = [x,y] & z in F . i & i in I )

proof

let z be object ; :: thesis: ( z in union (rng F) implies ex x, y, i being object st
( z = [x,y] & z in F . i & i in I ) )
assume z in union (rng F) ; :: thesis: ex x, y, i being object st
( z = [x,y] & z in F . i & i in I )
then consider Z being set such that
P02: ( z in Z & Z in rng F ) by TARSKI:def 4;
consider i being object such that
P03: ( i in dom F & Z = F . i ) by P02, FUNCT_1:def 3;
consider f being Function such that
P05: ( f = F . i & dom f = D . i & rng f = R . i ) by P03, A1;
ex x, y being object st z = [x,y] by P02, P03, P05, RELAT_1:def 1;
hence ex x, y, i being object st
( z = [x,y] & z in F . i & i in I ) by P02, P03; :: thesis: verum

end;

for z being object st z in union (rng F) holds
ex x, y being object st z = [x,y]

proof

let z be object ; :: thesis: ( z in union (rng F) implies ex x, y being object st z = [x,y] )
assume z in union (rng F) ; :: thesis: ex x, y being object st z = [x,y]
then ex x, y, i being object st
( z = [x,y] & z in F . i & i in I ) by P1;
hence ex x, y being object st z = [x,y] ; :: thesis: verum

end;

then reconsider G = union (rng F) as Relation by RELAT_1:def 1;
G is Function

proof

for x, y1, y2 being object st [x,y1] in G & [x,y2] in G holds
y1 = y2

proof

let x, y1, y2 be object ; :: thesis: ( [x,y1] in G & [x,y2] in G implies y1 = y2 )
assume P01: ( [x,y1] in G & [x,y2] in G ) ; :: thesis: y1 = y2
then consider a1, b1, i being object such that
P02: ( [x,y1] = [a1,b1] & [x,y1] in F . i & i in I ) by P1;
consider a2, b2, j being object such that
P03: ( [x,y2] = [a2,b2] & [x,y2] in F . j & j in I ) by P1, P01;
consider f being Function such that
P04: ( f = F . i & dom f = D . i & rng f = R . i ) by A1, P02;
consider g being Function such that
P05: ( g = F . j & dom g = D . j & rng g = R . j ) by A1, P03;
i = j

proof

assume Q04: i <> j ; :: thesis: contradiction
P041: x in D . i by P02, P04, XTUPLE_0:def 12;
P042: x in D . j by P03, P05, XTUPLE_0:def 12;
(D . i) /\ (D . j) = {} by P02, P03, P04, P05, Q04, A2, XBOOLE_0:def 7;
hence contradiction by P041, P042, XBOOLE_0:def 4; :: thesis: verum

end;

hence y1 = y2 by P02, P03, P04, FUNCT_1:def 1; :: thesis: verum

end;

hence G is Function by FUNCT_1:def 1; :: thesis: verum

end;

then reconsider G = G as Function ;
take G ; :: thesis: ( G = union (rng F) & dom G = union (rng D) & rng G = union (rng R) & ( for i, x being object
for f being Function st i in I & f = F . i & x in dom f holds
G . x = f . x ) )
thus G = union (rng F) ; :: thesis: ( dom G = union (rng D) & rng G = union (rng R) & ( for i, x being object
for f being Function st i in I & f = F . i & x in dom f holds
G . x = f . x ) )
for x being object holds
( x in dom G iff x in union (rng D) )

proof

let x be object ; :: thesis: ( x in dom G iff x in union (rng D) )

hereby :: thesis: ( x in union (rng D) implies x in dom G )

assume x in dom G ; :: thesis: x in union (rng D)
then consider y being object such that
S2: [x,y] in G by XTUPLE_0:def 12;
consider a, b, i being object such that
S3: ( [x,y] = [a,b] & [x,y] in F . i & i in I ) by P1, S2;
consider f being Function such that
S4: ( f = F . i & dom f = D . i & rng f = R . i ) by A1, S3;
S5: x in D . i by S3, S4, XTUPLE_0:def 12;
D . i in rng D by Q0, S3, FUNCT_1:3;
hence x in union (rng D) by S5, TARSKI:def 4; :: thesis: verum

end;

assume x in union (rng D) ; :: thesis: x in dom G
then consider Z being set such that
S6: ( x in Z & Z in rng D ) by TARSKI:def 4;
consider i being object such that
S7: ( i in dom D & Z = D . i ) by S6, FUNCT_1:def 3;
consider f being Function such that
S9: ( f = F . i & dom f = D . i & rng f = R . i ) by S7, A1;
consider y being object such that
S11: [x,y] in f by S6, S7, S9, XTUPLE_0:def 12;
F . i in rng F by FUNCT_1:3, P0, S7;
then [x,y] in G by S9, S11, TARSKI:def 4;
hence x in dom G by XTUPLE_0:def 12; :: thesis: verum

end;

hence dom G = union (rng D) by TARSKI:2; :: thesis: ( rng G = union (rng R) & ( for i, x being object
for f being Function st i in I & f = F . i & x in dom f holds
G . x = f . x ) )
for x being object holds
( x in rng G iff x in union (rng R) )

proof

let x be object ; :: thesis: ( x in rng G iff x in union (rng R) )

hereby :: thesis: ( x in union (rng R) implies x in rng G )

assume x in rng G ; :: thesis: x in union (rng R)
then consider y being object such that
S2: [y,x] in G by XTUPLE_0:def 13;
consider a, b, i being object such that
S3: ( [y,x] = [a,b] & [y,x] in F . i & i in I ) by P1, S2;
consider f being Function such that
S4: ( f = F . i & dom f = D . i & rng f = R . i ) by A1, S3;
S5: x in R . i by S3, S4, XTUPLE_0:def 13;
R . i in rng R by R0, S3, FUNCT_1:3;
hence x in union (rng R) by S5, TARSKI:def 4; :: thesis: verum

end;

assume x in union (rng R) ; :: thesis: x in rng G
then consider Z being set such that
S6: ( x in Z & Z in rng R ) by TARSKI:def 4;
consider i being object such that
S7: ( i in dom R & Z = R . i ) by S6, FUNCT_1:def 3;
consider f being Function such that
S9: ( f = F . i & dom f = D . i & rng f = R . i ) by S7, A1;
consider y being object such that
S11: [y,x] in f by S6, S7, S9, XTUPLE_0:def 13;
F . i in rng F by FUNCT_1:3, P0, S7;
then [y,x] in G by S9, S11, TARSKI:def 4;
hence x in rng G by XTUPLE_0:def 13; :: thesis: verum

end;

hence rng G = union (rng R) by TARSKI:2; :: thesis: for i, x being object
for f being Function st i in I & f = F . i & x in dom f holds
G . x = f . x
thus for i, x being object
for f being Function st i in I & f = F . i & x in dom f holds
G . x = f . x :: thesis: verum

proof

let i, x be object ; :: thesis: for f being Function st i in I & f = F . i & x in dom f holds
G . x = f . x
let f be Function; :: thesis: ( i in I & f = F . i & x in dom f implies G . x = f . x )
assume A1: ( i in I & f = F . i & x in dom f ) ; :: thesis: G . x = f . x
then P2: [x,(f . x)] in F . i by FUNCT_1:1;
F . i in rng F by FUNCT_1:3, A1, P0;
then [x,(f . x)] in G by P2, TARSKI:def 4;
hence G . x = f . x by FUNCT_1:1; :: thesis: verum

end;