let R, S, T be non empty RelStr ; :: thesis: for X being Subset of R
for f being Function of R,S
for g being Function of S,T st f preserves_sup_of X & g preserves_sup_of f .: X holds
g * f preserves_sup_of X
let X be Subset of R; :: thesis: for f being Function of R,S
for g being Function of S,T st f preserves_sup_of X & g preserves_sup_of f .: X holds
g * f preserves_sup_of X
let f be Function of R,S; :: thesis: for g being Function of S,T st f preserves_sup_of X & g preserves_sup_of f .: X holds
g * f preserves_sup_of X
let g be Function of S,T; :: thesis: ( f preserves_sup_of X & g preserves_sup_of f .: X implies g * f preserves_sup_of X )
assume that
A1: ( ex_sup_of X,R implies ( ex_sup_of f .: X,S & sup (f .: X) = f . (sup X) ) ) and
A2: ( ex_sup_of f .: X,S implies ( ex_sup_of g .: (f .: X),T & sup (g .: (f .: X)) = g . (sup (f .: X)) ) ) ; :: according to WAYBEL_0:def 31 :: thesis: g * f preserves_sup_of X
A3: g .: (f .: X) = (g * f) .: X by RELAT_1:126;
assume ex_sup_of X,R ; :: according to WAYBEL_0:def 31 :: thesis: ( ex_sup_of (g * f) .: X,T & "\/" (((g * f) .: X),T) = (g * f) . ("\/" (X,R)) )
hence ( ex_sup_of (g * f) .: X,T & "\/" (((g * f) .: X),T) = (g * f) . ("\/" (X,R)) ) by A1, A2, A3, FUNCT_2:15; :: thesis: verum