let L1, L2, L3 be complete LATTICE; :: thesis: for d1 being sups-preserving Function of L1,L2
for d2 being sups-preserving Function of L2,L3 holds UpperAdj (d2 * d1) = (UpperAdj d1) * (UpperAdj d2)
let d1 be sups-preserving Function of L1,L2; :: thesis: for d2 being sups-preserving Function of L2,L3 holds UpperAdj (d2 * d1) = (UpperAdj d1) * (UpperAdj d2)
let d2 be sups-preserving Function of L2,L3; :: thesis: UpperAdj (d2 * d1) = (UpperAdj d1) * (UpperAdj d2)
( [(UpperAdj d1),d1] is Galois & [(UpperAdj d2),d2] is Galois ) by Def2;
then ( [((UpperAdj d1) * (UpperAdj d2)),(d2 * d1)] is Galois & d2 * d1 is sups-preserving ) by WAYBEL15:7, WAYBEL20:28;
hence UpperAdj (d2 * d1) = (UpperAdj d1) * (UpperAdj d2) by Def2; :: thesis: verum