let L1, L2, L3 be non empty RelStr ; for f being Function of L1,L2
for g being Function of L2,L3 st f is sups-preserving & g is sups-preserving holds
g * f is sups-preserving
let f be Function of L1,L2; for g being Function of L2,L3 st f is sups-preserving & g is sups-preserving holds
g * f is sups-preserving
let g be Function of L2,L3; ( f is sups-preserving & g is sups-preserving implies g * f is sups-preserving )
assume that
A1:
f is sups-preserving
and
A2:
g is sups-preserving
; g * f is sups-preserving
set gf = g * f;
let X be Subset of L1; WAYBEL_0:def 33 g * f preserves_sup_of X
assume A3:
ex_sup_of X,L1
; WAYBEL_0:def 31 ( ex_sup_of (g * f) .: X,L3 & "\/" (((g * f) .: X),L3) = (g * f) . ("\/" (X,L1)) )
set fX = f .: X;
set gfX = (g * f) .: X;
A4:
f preserves_sup_of X
by A1;
then A5:
( (g * f) .: X = g .: (f .: X) & ex_sup_of f .: X,L2 )
by A3, RELAT_1:126;
A6:
dom f = the carrier of L1
by FUNCT_2:def 1;
A7:
g preserves_sup_of f .: X
by A2;
hence
ex_sup_of (g * f) .: X,L3
by A5; "\/" (((g * f) .: X),L3) = (g * f) . ("\/" (X,L1))
thus sup ((g * f) .: X) =
g . (sup (f .: X))
by A7, A5
.=
g . (f . (sup X))
by A3, A4
.=
(g * f) . (sup X)
by A6, FUNCT_1:13
; verum