let f be Function; :: thesis:
assume A1: dom f is subset-closed ; :: thesis:

hereby :: thesis:

assume A2: f is U-continuous ; :: thesis:
then A3: ( dom f is d.union-closed & f is d.union-distributive Function ) ;
hence ( dom f is d.union-closed & f is c=-monotone ) ; :: thesis:
reconsider C = dom f as subset-closed d.union-closed set by A1, A2;
let a, y be set ; :: thesis:
assume A4: ( a in dom f & y in f . a ) ; :: thesis:
reconsider A = { b where b is Subset of a : b is finite } as set ;
A5: A is c=directed

let Y be finite Subset of A; :: according to COHSP_1:def 4 :: thesis:
take union Y ; :: thesis:

let b be set ; :: thesis:
assume b in Y ; :: thesis:
then b in A ;
then ex c being Subset of a st
( b = c & c is finite ) ;
hence b is finite ; :: thesis:

end;

then A6: union Y is finite by FINSET_1:25;

let x be set ; :: thesis:
assume x in Y ; :: thesis:
then x in A ;
then ex c being Subset of a st
( x = c & c is finite ) ;
hence x c= a ; :: thesis:

end;

then union Y c= a by ZFMISC_1:94;
hence ( union Y c= union Y & union Y in A ) by A6; :: thesis:

end;

A c= C

let x be set ; :: according to TARSKI:def 3 :: thesis:
assume x in A ; :: thesis:
then ex b being Subset of a st
( x = b & b is finite ) ;
hence x in C by A4, CLASSES1:def 1; :: thesis:

end;

then ( A is Subset of C & union A in C ) by A5, Def7;
then A7: f . (union A) = union (f .: A) by A3, A5, Def11;
union A = a

thus union A c= a :: according to XBOOLE_0:def 10 :: thesis:

let x be set ; :: according to TARSKI:def 3 :: thesis:
assume x in union A ; :: thesis:
then consider b being set such that
A8: ( x in b & b in A ) by TARSKI:def 4;
ex c being Subset of a st
( b = c & c is finite ) by A8;
hence x in a by A8; :: thesis:

end;

let x be set ; :: according to TARSKI:def 3 :: thesis:
assume x in a ; :: thesis:
then {x} c= a by ZFMISC_1:37;
then ( x in {x} & {x} in A ) by TARSKI:def 1;
hence x in union A by TARSKI:def 4; :: thesis:

end;

then consider B being set such that
A9: ( y in B & B in f .: A ) by A4, A7, TARSKI:def 4;
consider b being set such that
A10: ( b in dom f & b in A & B = f . b ) by A9, FUNCT_1:def 12;
take b = b; :: thesis:
ex c being Subset of a st
( b = c & c is finite ) by A10;
hence ( b is finite & b c= a & y in f . b ) by A9, A10; :: thesis:

end;

assume dom f is d.union-closed ; :: thesis:
then reconsider C = dom f as d.union-closed set ;
assume that
A11: for a, b being set st a in dom f & b in dom f & a c= b holds
f . a c= f . b and
A12: for a, y being set st a in dom f & y in f . a holds
ex b being set st
( b is finite & b c= a & y in f . b ) ; :: according to COHSP_1:def 12 :: thesis:
C is d.union-closed ;
hence dom f is d.union-closed ; :: according to COHSP_1:def 14 :: thesis:
thus f is d.union-distributive :: thesis:

let A be Subset of (dom f); :: according to COHSP_1:def 11 :: thesis:
assume A13: ( A is c=directed & union A in dom f ) ; :: thesis:
reconsider A' = A as Subset of C ;
thus f . (union A) c= union (f .: A) :: according to XBOOLE_0:def 10 :: thesis:

let x be set ; :: according to TARSKI:def 3 :: thesis:
assume x in f . (union A) ; :: thesis:
then consider b being set such that
A14: ( b is finite & b c= union A' & x in f . b ) by A12, A13;
A' is c=directed set by A13;
then consider c being set such that
A15: ( c in A & b c= c ) by A14, Th13;
( b in C & c in C ) by A1, A15, CLASSES1:def 1;
then f . b c= f . c by A11, A15;
then ( x in f . c & f . c in f .: A ) by A14, A15, FUNCT_1:def 12;
hence x in union (f .: A) by TARSKI:def 4; :: thesis:

end;

let x be set ; :: according to TARSKI:def 3 :: thesis:
assume x in union (f .: A) ; :: thesis:
then consider B being set such that
A16: ( x in B & B in f .: A ) by TARSKI:def 4;
consider b being set such that
A17: ( b in dom f & b in A & B = f . b ) by A16, FUNCT_1:def 12;
B c= f . (union A') by A11, A13, A17, ZFMISC_1:92;
hence x in f . (union A) by A16; :: thesis:

end;