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

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
consider xx being set ;
for X1 being Ideal of L1 holds f preserves_sup_of X1 by A1, WAYBEL_0:def 37;
then A6: ( not f .: X is empty & f .: X is directed ) by A3, WAYBEL_0:72, YELLOW_2:17;

now

assume A7: ex_sup_of X,L1 ; :: thesis: ( ex_sup_of (g * f) .: X,L3 & sup ((g * f) .: X) = (g * f) . (sup X) )
f preserves_sup_of X by A1, A3, WAYBEL_0:def 37;
then A8: ( ex_sup_of f .: X,L2 & sup (f .: X) = f . (sup X) ) by A7, WAYBEL_0:def 31;
g preserves_sup_of f .: X by A2, A6, WAYBEL_0:def 37;
then A9: ( ex_sup_of g .: (f .: X),L3 & sup (g .: (f .: X)) = g . (sup (f .: X)) ) by A8, WAYBEL_0:def 31;
hence ex_sup_of (g * f) .: X,L3 by RELAT_1:159; :: thesis: sup ((g * f) .: X) = (g * f) . (sup X)
( sup X in the carrier of L1 & not the carrier of L2 is empty ) ;
then A10: sup X in dom f by FUNCT_2:def 1;
thus sup ((g * f) .: X) = g . (f . (sup X)) by A8, A9, RELAT_1:159
.= (g * f) . (sup X) by A10, FUNCT_1:23 ; :: 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