let C1, C2 be Coherence_Space; :: thesis:
let X be Subset of [:C1,(union C2):]; :: thesis:
assume that
A1: for x being set st x in X holds
x `1 is finite and
A2: for a, b being Element of C1 st a \/ b in C1 holds
for y1, y2 being set st [a,y1] in X & [b,y2] in X holds
{y1,y2} in C2 and
A3: for a, b being Element of C1 st a \/ b in C1 holds
for y being set st [a,y] in X & [b,y] in X holds
a = b ; :: thesis:
deffunc H₁( set ) -> set = X .: (Fin $1);
consider f being Function such that
A4: ( dom f = C1 & ( for a being set st a in C1 holds
f . a = H₁(a) ) ) from FUNCT_1:sch 3();
A5: rng f c= C2

let x be set ; :: according to TARSKI:def 3 :: thesis:
assume x in rng f ; :: thesis:
then consider a being set such that
A6: ( a in dom f & x = f . a ) by FUNCT_1:def 5;
reconsider a = a as Element of C1 by A4, A6;
A7: x = X .: (Fin a) by A4, A6;

let z, y be set ; :: thesis:
assume z in x ; :: thesis:
then consider z1 being set such that
A8: ( [z1,z] in X & z1 in Fin a ) by A7, RELAT_1:def 13;
assume y in x ; :: thesis:
then consider y1 being set such that
A9: ( [y1,y] in X & y1 in Fin a ) by A7, RELAT_1:def 13;
( z1 is finite Element of C1 & z1 \/ y1 in Fin a & y1 is finite Element of C1 ) by A8, A9, FINSUB_1:10;
hence {z,y} in C2 by A2, A8, A9; :: thesis:

end;

hence x in C2 by COH_SP:6; :: thesis:

end;

A10: f is c=-monotone

let a, b be set ; :: according to COHSP_1:def 12 :: thesis:
assume A11: ( a in dom f & b in dom f & a c= b ) ; :: thesis:
then reconsider a = a, b = b as Element of C1 by A4;
Fin a c= Fin b by A11, FINSUB_1:23;
then ( X .: (Fin a) c= X .: (Fin b) & f . a = X .: (Fin a) ) by A4, RELAT_1:156;
hence f . a c= f . b by A4; :: thesis:

end;

now

let a, y be set ; :: thesis:
assume A12: ( a in dom f & y in f . a ) ; :: thesis:
then y in X .: (Fin a) by A4;
then consider x being set such that
A13: ( [x,y] in X & x in Fin a ) by RELAT_1:def 13;
reconsider a' = a as Element of C1 by A4, A12;
take x = x; :: thesis:
x c= a by A13, FINSUB_1:def 5;
then ( x in C1 & x is finite ) by A4, A12, A13, CLASSES1:def 1;
then ( f . x = X .: (Fin x) & x in Fin x ) by A4, FINSUB_1:def 5;
hence ( x is finite & x c= a & y in f . x ) by A13, FINSUB_1:def 5, RELAT_1:def 13; :: thesis:
let c be set ; :: thesis:
assume A14: ( c c= a & y in f . c ) ; :: thesis:
then c c= a' ;
then c in dom f by A4, CLASSES1:def 1;
then y in X .: (Fin c) by A4, A14;
then consider z being set such that
A15: ( [z,y] in X & z in Fin c ) by RELAT_1:def 13;
Fin c c= Fin a by A14, FINSUB_1:23;
then ( z in Fin a' & x in Fin a' ) by A13, A15;
then ( x \/ z in Fin a' & z in C1 & x in C1 ) by FINSUB_1:10;
then x = z by A3, A13, A15;
hence x c= c by A15, FINSUB_1:def 5; :: thesis:

end;

then reconsider f = f as U-stable Function of C1,C2 by A4, A5, A10, Th23, FUNCT_2:def 1, RELSET_1:11;
take f ; :: thesis:
thus X = Trace f :: thesis:

let a, b be set ; :: according to RELAT_1:def 2 :: thesis:

hereby :: thesis:

assume A16: [a,b] in X ; :: thesis:
then ( [a,b] in [:C1,(union C2):] & [a,b] `1 = a ) by MCART_1:7;
then reconsider a' = a as finite Element of C1 by A1, A16, ZFMISC_1:106;
a' in Fin a by FINSUB_1:def 5;
then A17: ( b in X .: (Fin a) & f . a' = X .: (Fin a) ) by A4, A16, RELAT_1:def 13;

let c be set ; :: thesis:
assume A18: ( c in dom f & c c= a' & b in f . c ) ; :: thesis:
then reconsider c' = c as Element of C1 by A4;
b in X .: (Fin c') by A4, A18;
then consider x being set such that
A19: ( [x,b] in X & x in Fin c' ) by RELAT_1:def 13;
A20: x c= c by A19, FINSUB_1:def 5;
then x \/ a' = a' by A18, XBOOLE_1:1, XBOOLE_1:12;
then x = a by A3, A16, A19;
hence a' = c by A18, A20, XBOOLE_0:def 10; :: thesis:

end;

hence [a,b] in Trace f by A4, A17, Th32; :: thesis:

end;

assume A21: [a,b] in Trace f ; :: thesis:
then ( a in dom f & b in f . a ) by Th32;
then b in X .: (Fin a) by A4;
then consider x being set such that
A22: ( [x,b] in X & x in Fin a ) by RELAT_1:def 13;
reconsider a = a as Element of C1 by A4, A21, Th32;
x in Fin a by A22;
then reconsider x = x as finite Element of C1 ;
x in Fin x by FINSUB_1:def 5;
then b in X .: (Fin x) by A22, RELAT_1:def 13;
then ( b in f . x & x c= a ) by A4, A22, FINSUB_1:def 5;
hence [a,b] in X by A4, A21, A22, Th32; :: thesis:

end;

thus for a being Element of C1 holds f . a = X .: (Fin a) by A4; :: thesis: