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 ;
consider f being Function such that
P05: ( f = F . i & dom f = D . i & rng f = R . i ) by ;
ex x, y being object st z = [x,y] by ;
hence ex x, y, i being object st
( z = [x,y] & z in F . i & i in I ) by ; :: 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 ;
consider f being Function such that
P04: ( f = F . i & dom f = D . i & rng f = R . i ) by ;
consider g being Function such that
P05: ( g = F . j & dom g = D . j & rng g = R . j ) by ;
i = j
proof
assume Q04: i <> j ; :: thesis: contradiction
P041: x in D . i by ;
P042: x in D . j by ;
(D . i) /\ (D . j) = {} by ;
hence contradiction by P041, P042, XBOOLE_0:def 4; :: thesis: verum
end;
hence y1 = y2 by ; :: 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 ;
D . i in rng D by ;
hence x in union (rng D) by ; :: 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 ;
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 ;
F . i in rng F by ;
then [x,y] in G by ;
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 ;
R . i in rng R by ;
hence x in union (rng R) by ; :: 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 ;
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 ;
F . i in rng F by ;
then [y,x] in G by ;
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 ;
then [x,(f . x)] in G by ;
hence G . x = f . x by FUNCT_1:1; :: thesis: verum
end;