let S, T be lower-bounded with_suprema Poset; :: thesis: for f being Function of S,T st f is join-preserving & f is bottom-preserving holds
f is finite-sups-preserving
let f be Function of S,T; :: thesis: ( f is join-preserving & f is bottom-preserving implies f is finite-sups-preserving )
assume A1: ( f is join-preserving & f is bottom-preserving ) ; :: thesis: f is finite-sups-preserving
let X be finite Subset of S; :: according to WAYBEL34:def 15 :: thesis: f preserves_sup_of X
A2: X is finite ;
defpred S₁[ set ] means for Y being finite Subset of S st Y = $1 holds
f preserves_sup_of Y;
f preserves_sup_of {} S by A1;
then A3: S₁[ {} ] ;
A4: for x, B being set st x in X & B c= X & S₁[B] holds
S₁[B \/ {x}]

proof

let x, B be set ; :: thesis: ( x in X & B c= X & S₁[B] implies S₁[B \/ {x}] )
assume that
x in X and
B c= X and
A5: for Y being finite Subset of S st Y = B holds
f preserves_sup_of Y ; :: thesis: S₁[B \/ {x}]
let Y be finite Subset of S; :: thesis: ( Y = B \/ {x} implies f preserves_sup_of Y )
assume A6: Y = B \/ {x} ; :: thesis: f preserves_sup_of Y
A7: B c= Y by A6, XBOOLE_1:7;
A8: {x} c= Y by A6, XBOOLE_1:7;
reconsider Z = B as finite Subset of S by A7, XBOOLE_1:1;
A9: x in Y by A8, ZFMISC_1:31;
then reconsider x = x as Element of S ;
A10: f preserves_sup_of Z by A5;
( f .: Z = {} or ( f .: Z <> {} & f .: Z is finite ) ) ;
then A11: ex_sup_of f .: Z,T by YELLOW_0:42, YELLOW_0:54;
A12: ex_sup_of {(f . x)},T by YELLOW_0:54;
( Z = {} or Z <> {} ) ;
then A13: ex_sup_of Z,S by YELLOW_0:42, YELLOW_0:54;
A14: f preserves_sup_of {(sup Z),x} by A1;
A15: sup {x} = x by YELLOW_0:39;
A16: ex_sup_of {x},S by YELLOW_0:38;
A17: ex_sup_of Y,S by A9, YELLOW_0:54;
assume ex_sup_of Y,S ; :: according to WAYBEL_0:def 31 :: thesis: ( ex_sup_of f .: Y,T & "\/" ((f .: Y),T) = f . ("\/" (Y,S)) )
thus ex_sup_of f .: Y,T by A9, YELLOW_0:54; :: thesis: "\/" ((f .: Y),T) = f . ("\/" (Y,S))
dom f = the carrier of S by FUNCT_2:def 1;
then Im (f,x) = {(f . x)} by FUNCT_1:59;
then A18: f .: Y = (f .: Z) \/ {(f . x)} by A6, RELAT_1:120;
sup {(f . x)} = f . x by YELLOW_0:39;
hence sup (f .: Y) = (sup (f .: Z)) "\/" (f . x) by A11, A12, A18, YELLOW_2:3
.= (f . (sup Z)) "\/" (f . x) by A10, A13
.= f . ((sup Z) "\/" x) by A14, YELLOW_3:9
.= f . (sup Y) by A6, A13, A15, A16, A17, YELLOW_0:36 ;
:: thesis: verum

end;

S₁[X] from FINSET_1:sch 2(A2, A3, A4);
hence f preserves_sup_of X ; :: thesis: verum