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

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

hence
g * f is directed-sups-preserving
by WAYBEL_0:def 37; :: thesis: verumg * 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;

end;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) ) )

hence
g * f preserves_sup_of X
by WAYBEL_0:def 31; :: thesis: verum
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;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