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

( f is directed-sups-preserving & g is directed-sups-preserving ) by WAYBEL16:def 1;

then A1: g * f is directed-sups-preserving by WAYBEL20:28;

( f is infs-preserving & g is infs-preserving ) by WAYBEL16:def 1;

then g * f is infs-preserving by WAYBEL20:25;

hence g * f is CLHomomorphism of L,T by A1, WAYBEL16:def 1; :: thesis: verum

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

( f is directed-sups-preserving & g is directed-sups-preserving ) by WAYBEL16:def 1;

then A1: g * f is directed-sups-preserving by WAYBEL20:28;

( f is infs-preserving & g is infs-preserving ) by WAYBEL16:def 1;

then g * f is infs-preserving by WAYBEL20:25;

hence g * f is CLHomomorphism of L,T by A1, WAYBEL16:def 1; :: thesis: verum