let C1, C2 be Coherence_Space; :: thesis:
let X be Subset of [:(union C1),(union C2):]; :: thesis:
assume that
A1: for a, b being set 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
A2: for a, b being set 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 .: $1;
consider f being Function such that
A3: ( dom f = C1 & ( for a being set st a in C1 holds
f . a = H₁(a) ) ) from FUNCT_1:sch 3();
A4: rng f c= C2

proof

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

now

let z, y be set ; :: thesis:
assume z in x ; :: thesis:
then consider z1 being set such that
A7: ( [z1,z] in X & z1 in a ) by A6, RELAT_1:def 13;
assume y in x ; :: thesis:
then consider y1 being set such that
A8: ( [y1,y] in X & y1 in a ) by A6, RELAT_1:def 13;
{z1,y1} in C1 by A7, A8, COH_SP:6;
hence {z,y} in C2 by A1, A7, A8; :: thesis:

end;

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

end;

A9: f is c=-monotone

proof

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

end;

now

let a, y be set ; :: thesis:
assume A11: ( a in dom f & y in f . a ) ; :: thesis:
then y in X .: a by A3;
then consider x being set such that
A12: ( [x,y] in X & x in a ) by RELAT_1:def 13;
reconsider a' = a as Element of C1 by A3, A11;
take x = x; :: thesis:
{x} c= a by A12, ZFMISC_1:37;
then {x} in C1 by A3, A11, CLASSES1:def 1;
then ( x in {x} & f . {x} = X .: {x} ) by A3, TARSKI:def 1;
hence ( x in a & y in f . {x} ) by A12, RELAT_1:def 13; :: thesis:
let c be set ; :: thesis:
assume A13: ( c c= a & y in f . c ) ; :: thesis:
then c c= a' ;
then c in dom f by A3, CLASSES1:def 1;
then y in X .: c by A3, A13;
then consider z being set such that
A14: ( [z,y] in X & z in c ) by RELAT_1:def 13;
{x,z} c= a' by A12, A13, A14, ZFMISC_1:38;
then {x,z} in C1 by CLASSES1:def 1;
hence x in c by A2, A12, A14; :: thesis:

end;

then reconsider f = f as U-linear Function of C1,C2 by A3, A4, A9, Th24, FUNCT_2:def 1, RELSET_1:11;
take f ; :: thesis:
thus X = LinTrace f :: thesis:

proof

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

hereby :: thesis:

assume A15: [a,b] in X ; :: thesis:
then ( a in union C1 & b in union C2 ) by ZFMISC_1:106;
then consider a' being set such that
A16: ( a in a' & a' in C1 ) by TARSKI:def 4;
{a} c= a' by A16, ZFMISC_1:37;
then reconsider aa = {a} as Element of C1 by A16, CLASSES1:def 1;
a in {a} by TARSKI:def 1;
then A17: ( f . aa = X .: aa & b in X .: aa ) by A3, A15, RELAT_1:def 13;
f . {} = {} by Th19;
hence [a,b] in LinTrace f by A3, A17, Th52; :: thesis:

end;

assume [a,b] in LinTrace f ; :: thesis:
then ( {a} in dom f & b in f . {a} ) by Th53;
then b in X .: {a} by A3;
then consider x being set such that
A18: ( [x,b] in X & x in {a} ) by RELAT_1:def 13;
thus [a,b] in X by A18, TARSKI:def 1; :: thesis:

end;

thus for a being Element of C1 holds f . a = X .: a by A3; :: thesis: