let L, S, T be non empty complete Poset; :: thesis: for f being CLHomomorphism of L,S
for g being CLHomomorphism of S,T holds g * f is CLHomomorphism of L,T
let f be CLHomomorphism of L,S; :: thesis: for g being CLHomomorphism of S,T holds g * f is CLHomomorphism of L,T
let g be CLHomomorphism of S,T; :: thesis: g * f is CLHomomorphism of L,T
A1: ( f is infs-preserving & g is infs-preserving & f is directed-sups-preserving & g is directed-sups-preserving ) by WAYBEL16:def 1;
then A2: g * f is infs-preserving by WAYBEL20:26;
g * f is directed-sups-preserving by A1, WAYBEL20:29;
hence g * f is CLHomomorphism of L,T by A2, WAYBEL16:def 1; :: thesis: verum