let C1, C2 be Coherence_Space; :: thesis: for X being Subset of [:(union C1),(union C2):] st ( for a, b being set st {a,b} in C1 holds
for y1, y2 being object st [a,y1] in X & [b,y2] in X holds
{y1,y2} in C2 ) & ( for a, b being set st {a,b} in C1 holds
for y being object st [a,y] in X & [b,y] in X holds
a = b ) holds
ex f being U-linear Function of C1,C2 st
( X = LinTrace f & ( for a being Element of C1 holds f . a = X .: a ) )
let X be Subset of [:(union C1),(union C2):]; :: thesis: ( ( for a, b being set st {a,b} in C1 holds
for y1, y2 being object st [a,y1] in X & [b,y2] in X holds
{y1,y2} in C2 ) & ( for a, b being set st {a,b} in C1 holds
for y being object st [a,y] in X & [b,y] in X holds
a = b ) implies ex f being U-linear Function of C1,C2 st
( X = LinTrace f & ( for a being Element of C1 holds f . a = X .: a ) ) )
assume that
A1: for a, b being set st {a,b} in C1 holds
for y1, y2 being object 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 object st [a,y] in X & [b,y] in X holds
a = b ; :: thesis: ex f being U-linear Function of C1,C2 st
( X = LinTrace f & ( for a being Element of C1 holds f . a = X .: a ) )
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 5();

A4: now :: thesis: for a, y being set st a in dom f & y in f . a holds
ex x being set st
( x in a & y in f . {x} & ( for c being set st c c= a & y in f . c holds
x in c ) )

let a, y be set ; :: thesis: ( a in dom f & y in f . a implies ex x being set st
( x in a & y in f . {x} & ( for c being set st c c= a & y in f . c holds
x in c ) ) )
assume that
A5: a in dom f and
A6: y in f . a ; :: thesis: ex x being set st
( x in a & y in f . {x} & ( for c being set st c c= a & y in f . c holds
x in c ) )
reconsider a9 = a as Element of C1 by A3, A5;
y in X .: a9 by A3, A6;
then consider x being object such that
A7: [x,y] in X and
A8: x in a9 by RELAT_1:def 13;
reconsider x = x as set by TARSKI:1;
take x = x; :: thesis: ( x in a & y in f . {x} & ( for c being set st c c= a & y in f . c holds
x in c ) )
{x} c= a9 by A8, ZFMISC_1:31;
then {x} in C1 by 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 A7, A8, RELAT_1:def 13; :: thesis: for c being set st c c= a & y in f . c holds
x in c
let c be set ; :: thesis: ( c c= a & y in f . c implies x in c )
assume that
A9: c c= a and
A10: y in f . c ; :: thesis: x in c
c c= a9 by A9;
then c in dom f by A3, CLASSES1:def 1;
then y in X .: c by A3, A10;
then consider z being object such that
A11: [z,y] in X and
A12: z in c by RELAT_1:def 13;
{x,z} c= a9 by A8, A9, A12, ZFMISC_1:32;
then {x,z} in C1 by CLASSES1:def 1;
hence x in c by A2, A7, A11, A12; :: thesis: verum

end;

A13: rng f c= C2

proof

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in rng f or x in C2 )
reconsider xx = x as set by TARSKI:1;
assume x in rng f ; :: thesis: x in C2
then consider a being object such that
A14: a in dom f and
A15: x = f . a by FUNCT_1:def 3;
reconsider a = a as Element of C1 by A3, A14;
A16: x = X .: a by A3, A15;

now :: thesis: for z, y being set st z in xx & y in xx holds
{z,y} in C2

let z, y be set ; :: thesis: ( z in xx & y in xx implies {z,y} in C2 )
assume z in xx ; :: thesis: ( y in xx implies {z,y} in C2 )
then consider z1 being object such that
A17: [z1,z] in X and
A18: z1 in a by A16, RELAT_1:def 13;
assume y in xx ; :: thesis: {z,y} in C2
then consider y1 being object such that
A19: [y1,y] in X and
A20: y1 in a by A16, RELAT_1:def 13;
A21: ( z1 is set & y1 is set ) by TARSKI:1;
{z1,y1} in C1 by A18, A20, COH_SP:6;
hence {z,y} in C2 by A1, A17, A19, A21; :: thesis: verum

end;

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

end;

f is c=-monotone

proof

let a, b be set ; :: according to COHSP_1:def 11 :: thesis: ( a in dom f & b in dom f & a c= b implies f . a c= f . b )
assume that
A22: ( a in dom f & b in dom f ) and
A23: a c= b ; :: thesis: f . a c= f . b
reconsider a = a, b = b as Element of C1 by A3, A22;
A24: f . a = X .: a by A3;
X .: a c= X .: b by A23, RELAT_1:123;
hence f . a c= f . b by A3, A24; :: thesis: verum

end;

then reconsider f = f as U-linear Function of C1,C2 by A3, A13, A4, Th23, FUNCT_2:def 1, RELSET_1:4;
take f ; :: thesis: ( X = LinTrace f & ( for a being Element of C1 holds f . a = X .: a ) )
thus X = LinTrace f :: thesis: for a being Element of C1 holds f . a = X .: a

proof

let a, b be object ; :: according to RELAT_1:def 2 :: thesis: ( ( not [a,b] in X or [a,b] in LinTrace f ) & ( not [a,b] in LinTrace f or [a,b] in X ) )

hereby :: thesis: ( not [a,b] in LinTrace f or [a,b] in X )

assume A25: [a,b] in X ; :: thesis: [a,b] in LinTrace f
then a in union C1 by ZFMISC_1:87;
then consider a9 being set such that
A26: a in a9 and
A27: a9 in C1 by TARSKI:def 4;
{a} c= a9 by A26, ZFMISC_1:31;
then reconsider aa = {a} as Element of C1 by A27, CLASSES1:def 1;
A28: ( f . aa = X .: aa & f . {} = {} ) by A3, Th18;
a in {a} by TARSKI:def 1;
then b in X .: aa by A25, RELAT_1:def 13;
hence [a,b] in LinTrace f by A3, A28, Th51; :: thesis: verum

end;

assume A29: [a,b] in LinTrace f ; :: thesis: [a,b] in X
then b in f . {a} by Th52;
then b in X .: {a} by A3, A29, Th52;
then ex x being object st
( [x,b] in X & x in {a} ) by RELAT_1:def 13;
hence [a,b] in X by TARSKI:def 1; :: thesis: verum

end;

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