let R, S, T be non empty RelStr ; :: thesis: for f being Function of R,S
for g being Function of S,T st f is finite-sups-preserving & g is finite-sups-preserving holds
g * f is finite-sups-preserving
let f be Function of R,S; :: thesis: for g being Function of S,T st f is finite-sups-preserving & g is finite-sups-preserving holds
g * f is finite-sups-preserving
let g be Function of S,T; :: thesis: ( f is finite-sups-preserving & g is finite-sups-preserving implies g * f is finite-sups-preserving )
assume that
A1: for X being finite Subset of R holds f preserves_sup_of X and
A2: for X being finite Subset of S holds g preserves_sup_of X ; :: according to WAYBEL34:def 15 :: thesis: g * f is finite-sups-preserving
let X be finite Subset of R; :: according to WAYBEL34:def 15 :: thesis: g * f preserves_sup_of X
g preserves_sup_of f .: X by A2;
hence g * f preserves_sup_of X by A1, Th58; :: thesis: verum