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 )

ex x, y being object st z = [x,y]

G is 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) )

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) )

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

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

for z being object st z in union (rng F) holds
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;( 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

ex x, y being object st z = [x,y]

proof

then reconsider G = union (rng F) as Relation by RELAT_1:def 1;
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;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

G is Function

proof

then reconsider G = G as Function ;
for x, y1, y2 being object st [x,y1] in G & [x,y2] in G holds

y1 = y2

end;y1 = y2

proof

hence
G is Function
by FUNCT_1:def 1; :: thesis: verum
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

end;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

hence
y1 = y2
by P02, P03, P04, FUNCT_1:def 1; :: thesis: verum
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;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

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

hence
dom G = union (rng D)
by TARSKI:2; :: thesis: ( rng G = union (rng R) & ( for i, x being object
let x be object ; :: thesis: ( x in dom G iff x in union (rng D) )

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;hereby :: thesis: ( x in union (rng D) implies x in dom G )

assume
x in union (rng D)
; :: thesis: x in dom Gassume
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;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

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

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

hence
rng G = union (rng R)
by TARSKI:2; :: thesis: for i, x being object
let x be object ; :: thesis: ( x in rng G iff x in union (rng R) )

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;hereby :: thesis: ( x in union (rng R) implies x in rng G )

assume
x in union (rng R)
; :: thesis: x in rng Gassume
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;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

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

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