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 3();
A5: rng f c= C2

proof

let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in rng f or x in C2 )
assume x in rng f ; :: thesis: x in C2
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;

now

let z, y be set ; :: thesis: ( z in x & y in x implies {z,y} in C2 )
assume z in x ; :: thesis: ( y in x implies {z,y} in C2 )
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: {z,y} in C2
then consider y1 being set such that
A9: ( [y1,y] in X & y1 in Fin a ) by A7, RELAT_1:def 13;
reconsider z1 = z1, y1 = y1 as finite Element of C1 by A8, A9;
z1 \/ y1 in Fin a by A8, A9, FINSUB_1:10;
then reconsider b = z1 \/ y1 as finite Element of C1 ;
( [b,z] in X & [b,y] in X ) by A2, A8, A9, XBOOLE_1:7;
hence {z,y} in C2 by A3; :: thesis: verum

end;

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

end;

A10: f is c=-monotone

proof

let a, b be set ; :: according to COHSP_1:def 12 :: thesis: ( a in dom f & b in dom f & a c= b implies f . a c= f . b )
assume A11: ( a in dom f & b in dom f & a c= b ) ; :: thesis: f . a c= f . b
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: verum

end;

now

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 A12: ( a in dom f & y in f . a ) ; :: thesis: ex x being set st
( x is finite & x c= a & y in f . x )
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;
take x = x; :: thesis: ( x is finite & x c= a & y in f . x )
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: verum

end;

then reconsider f = f as U-continuous Function of C1,C2 by A4, A5, A10, Th22, FUNCT_2:def 1, RELSET_1:11;
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 set ; :: 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 A14: [a,b] in X ; :: thesis: [a,b] in graph f
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, A14, ZFMISC_1:106;
a' in Fin a by FINSUB_1:def 5;
then ( b in X .: (Fin a) & f . a' = X .: (Fin a) ) by A4, A14, RELAT_1:def 13;
hence [a,b] in graph f by A4, Th25; :: thesis: verum

end;

assume A15: [a,b] in graph f ; :: thesis: [a,b] in X
then reconsider a = a as finite Element of C1 by A4, Th25;
( b in f . a & f . a = X .: (Fin a) ) by A4, A15, Th25;
then consider x being set such that
A16: ( [x,b] in X & x in Fin a ) by RELAT_1:def 13;
( x c= a & x is finite Element of C1 ) by A16, FINSUB_1:def 5;
hence [a,b] in X by A2, A16; :: thesis: verum

end;

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