let S, T be complete Scott TopLattice; :: thesis: for f being Function of S,T st S is algebraic & T is algebraic & ( for x being Element of S holds f . x = "\/" ( { (f . w) where w is Element of S : w << x } ,T) ) holds

for x being Element of S holds f . x = "\/" ( { (f . w) where w is Element of S : ( w <= x & w is compact ) } ,T)

let f be Function of S,T; :: thesis: ( S is algebraic & T is algebraic & ( for x being Element of S holds f . x = "\/" ( { (f . w) where w is Element of S : w << x } ,T) ) implies for x being Element of S holds f . x = "\/" ( { (f . w) where w is Element of S : ( w <= x & w is compact ) } ,T) )

assume that

A1: S is algebraic and

A2: T is algebraic ; :: thesis: ( ex x being Element of S st not f . x = "\/" ( { (f . w) where w is Element of S : w << x } ,T) or for x being Element of S holds f . x = "\/" ( { (f . w) where w is Element of S : ( w <= x & w is compact ) } ,T) )

A3: S is continuous by A1, WAYBEL_8:7;

A4: T is continuous by A2, WAYBEL_8:7;

assume A5: for x being Element of S holds f . x = "\/" ( { (f . w) where w is Element of S : w << x } ,T) ; :: thesis: for x being Element of S holds f . x = "\/" ( { (f . w) where w is Element of S : ( w <= x & w is compact ) } ,T)

let x be Element of S; :: thesis: f . x = "\/" ( { (f . w) where w is Element of S : ( w <= x & w is compact ) } ,T)

A6: the carrier of S c= dom f by FUNCT_2:def 1;

defpred S_{1}[ Element of S] means ( $1 <= x & $1 is compact );

deffunc H_{1}( Element of S) -> Element of S = $1;

A7: f .: { H_{1}(w) where w is Element of S : S_{1}[w] } = { (f . H_{1}(w)) where w is Element of S : S_{1}[w] }
from WAYBEL17:sch 1(A6);

A8: f .: { w where w is Element of S : ( w <= x & w is compact ) } = f .: (compactbelow x) by WAYBEL_8:def 2;

reconsider D = compactbelow x as non empty directed Subset of S by A1, WAYBEL_8:def 4;

f is directed-sups-preserving by A3, A4, A5, Lm16;

then A9: f preserves_sup_of D ;

A10: ex_sup_of D,S by YELLOW_0:17;

S is satisfying_axiom_K by A1, WAYBEL_8:def 4;

then f . x = f . (sup D) by WAYBEL_8:def 3

.= "\/" ( { (f . w) where w is Element of S : ( w <= x & w is compact ) } ,T) by A7, A8, A9, A10 ;

hence f . x = "\/" ( { (f . w) where w is Element of S : ( w <= x & w is compact ) } ,T) ; :: thesis: verum

for x being Element of S holds f . x = "\/" ( { (f . w) where w is Element of S : ( w <= x & w is compact ) } ,T)

let f be Function of S,T; :: thesis: ( S is algebraic & T is algebraic & ( for x being Element of S holds f . x = "\/" ( { (f . w) where w is Element of S : w << x } ,T) ) implies for x being Element of S holds f . x = "\/" ( { (f . w) where w is Element of S : ( w <= x & w is compact ) } ,T) )

assume that

A1: S is algebraic and

A2: T is algebraic ; :: thesis: ( ex x being Element of S st not f . x = "\/" ( { (f . w) where w is Element of S : w << x } ,T) or for x being Element of S holds f . x = "\/" ( { (f . w) where w is Element of S : ( w <= x & w is compact ) } ,T) )

A3: S is continuous by A1, WAYBEL_8:7;

A4: T is continuous by A2, WAYBEL_8:7;

assume A5: for x being Element of S holds f . x = "\/" ( { (f . w) where w is Element of S : w << x } ,T) ; :: thesis: for x being Element of S holds f . x = "\/" ( { (f . w) where w is Element of S : ( w <= x & w is compact ) } ,T)

let x be Element of S; :: thesis: f . x = "\/" ( { (f . w) where w is Element of S : ( w <= x & w is compact ) } ,T)

A6: the carrier of S c= dom f by FUNCT_2:def 1;

defpred S

deffunc H

A7: f .: { H

A8: f .: { w where w is Element of S : ( w <= x & w is compact ) } = f .: (compactbelow x) by WAYBEL_8:def 2;

reconsider D = compactbelow x as non empty directed Subset of S by A1, WAYBEL_8:def 4;

f is directed-sups-preserving by A3, A4, A5, Lm16;

then A9: f preserves_sup_of D ;

A10: ex_sup_of D,S by YELLOW_0:17;

S is satisfying_axiom_K by A1, WAYBEL_8:def 4;

then f . x = f . (sup D) by WAYBEL_8:def 3

.= "\/" ( { (f . w) where w is Element of S : ( w <= x & w is compact ) } ,T) by A7, A8, A9, A10 ;

hence f . x = "\/" ( { (f . w) where w is Element of S : ( w <= x & w is compact ) } ,T) ; :: thesis: verum