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 ;
A4: T is continuous by ;
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 S1[ Element of S] means ( \$1 <= x & \$1 is compact );
deffunc H1( Element of S) -> Element of S = \$1;
A7: f .: { H1(w) where w is Element of S : S1[w] } = { (f . H1(w)) where w is Element of S : S1[w] } from A8: f .: { w where w is Element of S : ( w <= x & w is compact ) } = f .: () by WAYBEL_8:def 2;
reconsider D = compactbelow x as non empty directed Subset of S by ;
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 ;
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