let L1, L2, L3 be non empty Poset; 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; 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; ( 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
; g * f is directed-sups-preserving
now for X being Subset of L1 st not X is empty & X is directed holds
g * f preserves_sup_of Xlet X be
Subset of
L1;
( not X is empty & X is directed implies g * f preserves_sup_of X )assume A3:
( not
X is
empty &
X is
directed )
;
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 ( 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
;
( 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;
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
;
verum end; hence
g * f preserves_sup_of X
by WAYBEL_0:def 31;
verum end;
hence
g * f is directed-sups-preserving
by WAYBEL_0:def 37; verum