let C1, C2 be Coherence_Space; :: thesis: for A being set st ( for x, y being set st x in A & y in A holds
ex f being U-stable Function of C1,C2 st x \/ y = Trace f ) holds
ex f being U-stable Function of C1,C2 st union A = Trace f
let A be set ; :: thesis: ( ( for x, y being set st x in A & y in A holds
ex f being U-stable Function of C1,C2 st x \/ y = Trace f ) implies ex f being U-stable Function of C1,C2 st union A = Trace f )
assume A1: for x, y being set st x in A & y in A holds
ex f being U-stable Function of C1,C2 st x \/ y = Trace f ; :: thesis: ex f being U-stable Function of C1,C2 st union A = Trace f
set X = union A;
A2: union A c= [:C1,(union C2):]

proof

let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in union A or x in [:C1,(union C2):] )
assume x in union A ; :: thesis: x in [:C1,(union C2):]
then consider y being set such that
A3: ( x in y & y in A ) by TARSKI:def 4;
y \/ y = y ;
then consider f being U-stable Function of C1,C2 such that
A4: y = Trace f by A1, A3;
thus x in [:C1,(union C2):] by A3, A4; :: thesis: verum

end;

A5: now

let x be set ; :: thesis: ( x in union A implies x `1 is finite )
assume x in union A ; :: thesis: x `1 is finite
then consider y being set such that
A6: ( x in y & y in A ) by TARSKI:def 4;
y \/ y = y ;
then consider f being U-stable Function of C1,C2 such that
A7: y = Trace f by A1, A6;
consider a, y being set such that
A8: ( x = [a,y] & a in dom f & y in f . a & ( for b being set st b in dom f & b c= a & y in f . b holds
a = b ) ) by A6, A7, Def18;
dom f = C1 by FUNCT_2:def 1;
then a is finite by A6, A7, A8, Th34;
hence x `1 is finite by A8, MCART_1:7; :: thesis: verum

end;

A9: now

let a, b be Element of C1; :: thesis: ( a \/ b in C1 implies for y1, y2 being set st [a,y1] in union A & [b,y2] in union A holds
{y1,y2} in C2 )
assume A10: a \/ b in C1 ; :: thesis: for y1, y2 being set st [a,y1] in union A & [b,y2] in union A holds
{y1,y2} in C2
let y1, y2 be set ; :: thesis: ( [a,y1] in union A & [b,y2] in union A implies {y1,y2} in C2 )
assume [a,y1] in union A ; :: thesis: ( [b,y2] in union A implies {y1,y2} in C2 )
then consider x1 being set such that
A11: ( [a,y1] in x1 & x1 in A ) by TARSKI:def 4;
assume [b,y2] in union A ; :: thesis: {y1,y2} in C2
then consider x2 being set such that
A12: ( [b,y2] in x2 & x2 in A ) by TARSKI:def 4;
consider f being U-stable Function of C1,C2 such that
A13: x1 \/ x2 = Trace f by A1, A11, A12;
( x1 c= x1 \/ x2 & x2 c= x1 \/ x2 ) by XBOOLE_1:7;
hence {y1,y2} in C2 by A10, A11, A12, A13, Th35; :: thesis: verum

end;

now

let a, b be Element of C1; :: thesis: ( a \/ b in C1 implies for y being set st [a,y] in union A & [b,y] in union A holds
a = b )
assume A14: a \/ b in C1 ; :: thesis: for y being set st [a,y] in union A & [b,y] in union A holds
a = b
let y be set ; :: thesis: ( [a,y] in union A & [b,y] in union A implies a = b )
assume [a,y] in union A ; :: thesis: ( [b,y] in union A implies a = b )
then consider x1 being set such that
A15: ( [a,y] in x1 & x1 in A ) by TARSKI:def 4;
assume [b,y] in union A ; :: thesis: a = b
then consider x2 being set such that
A16: ( [b,y] in x2 & x2 in A ) by TARSKI:def 4;
consider f being U-stable Function of C1,C2 such that
A17: x1 \/ x2 = Trace f by A1, A15, A16;
( x1 c= x1 \/ x2 & x2 c= x1 \/ x2 ) by XBOOLE_1:7;
hence a = b by A14, A15, A16, A17, Th36; :: thesis: verum

end;

hence ex f being U-stable Function of C1,C2 st union A = Trace f by A2, A5, A9, Th39; :: thesis: verum