let L1, L2, L3 be complete LATTICE; :: thesis: for g1 being infs-preserving Function of L1,L2
for g2 being infs-preserving Function of L2,L3 holds LowerAdj (g2 * g1) = (LowerAdj g1) * (LowerAdj g2)
let g1 be infs-preserving Function of L1,L2; :: thesis: for g2 being infs-preserving Function of L2,L3 holds LowerAdj (g2 * g1) = (LowerAdj g1) * (LowerAdj g2)
let g2 be infs-preserving Function of L2,L3; :: thesis: LowerAdj (g2 * g1) = (LowerAdj g1) * (LowerAdj g2)
A1: [g1,(LowerAdj g1)] is Galois by Def1;
[g2,(LowerAdj g2)] is Galois by Def1;
then A2: [(g2 * g1),((LowerAdj g1) * (LowerAdj g2))] is Galois by A1, WAYBEL15:5;
g2 * g1 is infs-preserving by WAYBEL20:25;
hence LowerAdj (g2 * g1) = (LowerAdj g1) * (LowerAdj g2) by A2, Def1; :: thesis: verum