let L1, L2, L3 be non empty reflexive antisymmetric RelStr ; :: 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
set gf = g * f;
let X be Subset of L1; :: according to WAYBEL_0:def 37 :: thesis: ( X is empty or not X is directed or g * f preserves_sup_of X )
assume that
A3: ( not X is empty & X is directed ) and
A4: ex_sup_of X,L1 ; :: according to WAYBEL_0:def 31 :: thesis: ( ex_sup_of (g * f) .: X,L3 & "\/" ((g * f) .: X),L3 = (g * f) . ("\/" X,L1) )
A5: dom f = the carrier of L1 by FUNCT_2:def 1;
set gfX = (g * f) .: X;
set fX = f .: X;
A6: f preserves_sup_of X by A1, A3, WAYBEL_0:def 37;
consider xx being Element of X;
( xx in X & X c= the carrier of L1 ) by A3;
then f . xx in f .: X by FUNCT_2:43;
then ( not f .: X is empty & f .: X is directed ) by A1, A3, WAYBEL17:3, YELLOW_2:17;
then A7: g preserves_sup_of f .: X by A2, WAYBEL_0:def 37;
A8: (g * f) .: X = g .: (f .: X) by RELAT_1:159;
A9: ex_sup_of f .: X,L2 by A4, A6, WAYBEL_0:def 31;
hence ex_sup_of (g * f) .: X,L3 by A7, A8, WAYBEL_0:def 31; :: thesis: "\/" ((g * f) .: X),L3 = (g * f) . ("\/" X,L1)
thus sup ((g * f) .: X) = g . (sup (f .: X)) by A7, A8, A9, WAYBEL_0:def 31
.= g . (f . (sup X)) by A4, A6, WAYBEL_0:def 31
.= (g * f) . (sup X) by A5, FUNCT_1:23 ; :: thesis: verum