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₁[ Element of S] means ( $1 <= x & $1 is compact );
deffunc H₁( Element of S) -> Element of S = $1;
A7: f .: { H₁(w) where w is Element of S : S₁[w] } = { (f . H₁(w)) where w is Element of S : S₁[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