let C1, C2 be Coherence_Space; :: thesis: for X being Subset of [:C1,(union C2):] st ( for x being set st x in X holds
x `1 is finite ) & ( for a, b being finite Element of C1 st a c= b holds
for y being set st [a,y] in X holds
[b,y] in X ) & ( for a being finite Element of C1
for y1, y2 being set st [a,y1] in X & [a,y2] in X holds
{y1,y2} in C2 ) holds
ex f being U-continuous Function of C1,C2 st
( X = graph f & ( for a being Element of C1 holds f . a = X .: (Fin a) ) )
let X be Subset of [:C1,(union C2):]; :: thesis: ( ( for x being set st x in X holds
x `1 is finite ) & ( for a, b being finite Element of C1 st a c= b holds
for y being set st [a,y] in X holds
[b,y] in X ) & ( for a being finite Element of C1
for y1, y2 being set st [a,y1] in X & [a,y2] in X holds
{y1,y2} in C2 ) implies ex f being U-continuous Function of C1,C2 st
( X = graph f & ( for a being Element of C1 holds f . a = X .: (Fin a) ) ) )
assume that
A1: for x being set st x in X holds
x `1 is finite and
A2: for a, b being finite Element of C1 st a c= b holds
for y being set st [a,y] in X holds
[b,y] in X and
A3: for a being finite Element of C1
for y1, y2 being set st [a,y1] in X & [a,y2] in X holds
{y1,y2} in C2 ; :: thesis: ex f being U-continuous Function of C1,C2 st
( X = graph f & ( for a being Element of C1 holds f . a = X .: (Fin a) ) )
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 5();
A5: 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
A6: a in dom f and
A7: x = f . a by FUNCT_1:def 3;
reconsider a = a as Element of C1 by A4, A6;
A8: x = X .: (Fin a) by A4, A7;

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
A9: [z1,z] in X and
A10: z1 in Fin a by A8, RELAT_1:def 13;
assume y in xx ; :: thesis: {z,y} in C2
then consider y1 being object such that
A11: [y1,y] in X and
A12: y1 in Fin a by A8, RELAT_1:def 13;
reconsider z1 = z1, y1 = y1 as finite Element of C1 by A10, A12;
z1 \/ y1 in Fin a by A10, A12, FINSUB_1:1;
then reconsider b = z1 \/ y1 as finite Element of C1 ;
A13: [b,y] in X by A2, A11, XBOOLE_1:7;
[b,z] in X by A2, A9, XBOOLE_1:7;
hence {z,y} in C2 by A3, A13; :: thesis: verum

end;

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

end;

A14: now :: thesis: for a, y being set st a in dom f & y in f . a holds
ex x being set st
( x is finite & x c= a & y in f . x )

let a, y be set ; :: thesis: ( a in dom f & y in f . a implies ex x being set st
( x is finite & x c= a & y in f . x ) )
assume that
A15: a in dom f and
A16: y in f . a ; :: thesis: ex x being set st
( x is finite & x c= a & y in f . x )
y in X .: (Fin a) by A4, A15, A16;
then consider x being object such that
A17: [x,y] in X and
A18: x in Fin a by RELAT_1:def 13;
reconsider x = x as set by TARSKI:1;
x c= a by A18, FINSUB_1:def 5;
then x in C1 by A4, A15, CLASSES1:def 1;
then A19: f . x = X .: (Fin x) by A4;
take x = x; :: thesis: ( x is finite & x c= a & y in f . x )
x in Fin x by A18, FINSUB_1:def 5;
hence ( x is finite & x c= a & y in f . x ) by A17, A18, A19, FINSUB_1:def 5, RELAT_1:def 13; :: 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
A20: ( a in dom f & b in dom f ) and
A21: a c= b ; :: thesis: f . a c= f . b
reconsider a = a, b = b as Element of C1 by A4, A20;
Fin a c= Fin b by A21, FINSUB_1:10;
then A22: X .: (Fin a) c= X .: (Fin b) by RELAT_1:123;
f . a = X .: (Fin a) by A4;
hence f . a c= f . b by A4, A22; :: thesis: verum

end;

then reconsider f = f as U-continuous Function of C1,C2 by A4, A5, A14, Th21, FUNCT_2:def 1, RELSET_1:4;
take f ; :: thesis: ( X = graph f & ( for a being Element of C1 holds f . a = X .: (Fin a) ) )
thus X = graph f :: thesis: for a being Element of C1 holds f . a = X .: (Fin a)

proof

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

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

assume A23: [a,b] in X ; :: thesis: [a,b] in graph f
[a,b] `1 = a ;
then reconsider a9 = a as finite Element of C1 by A1, A23, ZFMISC_1:87;
a9 in Fin a9 by FINSUB_1:def 5;
then A24: b in X .: (Fin a9) by A23, RELAT_1:def 13;
f . a9 = X .: (Fin a9) by A4;
hence [a,b] in graph f by A4, A24, Th24; :: thesis: verum

end;

A25: ( a is set & b is set ) by TARSKI:1;
assume A26: [a,b] in graph f ; :: thesis: [a,b] in X
then reconsider a = a as finite Element of C1 by A4, Th24, A25;
A27: f . a = X .: (Fin a) by A4;
b in f . a by A26, Th24, A25;
then consider x being object such that
A28: [x,b] in X and
A29: x in Fin a by A27, RELAT_1:def 13;
reconsider x = x as set by TARSKI:1;
x c= a by A29, FINSUB_1:def 5;
hence [a,b] in X by A2, A28, A29, A25; :: thesis: verum

end;

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