let L1, L2, L3 be non empty Poset; :: thesis: for f being Function of L1,L2
for g being Function of L2,L3 st f is directed-sups-preserving & g is directed-sups-preserving holds
g * f is directed-sups-preserving
let f be Function of L1,L2; :: thesis: for g being Function of L2,L3 st f is directed-sups-preserving & g is directed-sups-preserving holds
g * f is directed-sups-preserving
let g be Function of L2,L3; :: thesis: ( f is directed-sups-preserving & g is directed-sups-preserving implies g * f is directed-sups-preserving )
assume that
A1: f is directed-sups-preserving and
A2: g is directed-sups-preserving ; :: thesis: g * f is directed-sups-preserving

now :: thesis: for X being Subset of L1 st not X is empty & X is directed holds
g * f preserves_sup_of X

let X be Subset of L1; :: thesis: ( not X is empty & X is directed implies g * f preserves_sup_of X )
assume A3: ( not X is empty & X is directed ) ; :: thesis: g * f preserves_sup_of X
for X1 being Ideal of L1 holds f preserves_sup_of X1 by A1, WAYBEL_0:def 37;
then A4: ( not f .: X is empty & f .: X is directed ) by A3, WAYBEL_0:72, YELLOW_2:15;

now :: thesis: ( ex_sup_of X,L1 implies ( ex_sup_of (g * f) .: X,L3 & sup ((g * f) .: X) = (g * f) . (sup X) ) )

sup X in the carrier of L1 ;
then A5: sup X in dom f by FUNCT_2:def 1;
assume A6: ex_sup_of X,L1 ; :: thesis: ( ex_sup_of (g * f) .: X,L3 & sup ((g * f) .: X) = (g * f) . (sup X) )
A7: f preserves_sup_of X by A1, A3, WAYBEL_0:def 37;
then A8: ex_sup_of f .: X,L2 by A6, WAYBEL_0:def 31;
A9: g preserves_sup_of f .: X by A2, A4, WAYBEL_0:def 37;
then A10: sup (g .: (f .: X)) = g . (sup (f .: X)) by A8, WAYBEL_0:def 31;
ex_sup_of g .: (f .: X),L3 by A8, A9, WAYBEL_0:def 31;
hence ex_sup_of (g * f) .: X,L3 by RELAT_1:126; :: thesis: sup ((g * f) .: X) = (g * f) . (sup X)
sup (f .: X) = f . (sup X) by A6, A7, WAYBEL_0:def 31;
hence sup ((g * f) .: X) = g . (f . (sup X)) by A10, RELAT_1:126
.= (g * f) . (sup X) by A5, FUNCT_1:13 ;
:: thesis: verum

end;

hence g * f preserves_sup_of X by WAYBEL_0:def 31; :: thesis: verum

end;

hence g * f is directed-sups-preserving by WAYBEL_0:def 37; :: thesis: verum