let L1, L2, L3 be non empty Poset; :: thesis: for g1 being Function of L1,L2
for g2 being Function of L2,L3
for d1 being Function of L2,L1
for d2 being Function of L3,L2 st [g1,d1] is Galois & [g2,d2] is Galois holds
[(g2 * g1),(d1 * d2)] is Galois

let g1 be Function of L1,L2; :: thesis: for g2 being Function of L2,L3
for d1 being Function of L2,L1
for d2 being Function of L3,L2 st [g1,d1] is Galois & [g2,d2] is Galois holds
[(g2 * g1),(d1 * d2)] is Galois

let g2 be Function of L2,L3; :: thesis: for d1 being Function of L2,L1
for d2 being Function of L3,L2 st [g1,d1] is Galois & [g2,d2] is Galois holds
[(g2 * g1),(d1 * d2)] is Galois

let d1 be Function of L2,L1; :: thesis: for d2 being Function of L3,L2 st [g1,d1] is Galois & [g2,d2] is Galois holds
[(g2 * g1),(d1 * d2)] is Galois

let d2 be Function of L3,L2; :: thesis: ( [g1,d1] is Galois & [g2,d2] is Galois implies [(g2 * g1),(d1 * d2)] is Galois )
assume that
A1: [g1,d1] is Galois and
A2: [g2,d2] is Galois ; :: thesis: [(g2 * g1),(d1 * d2)] is Galois
A3: d1 is monotone by ;
A4: g2 is monotone by ;
A5: now :: thesis: for s being Element of L3
for t being Element of L1 holds
( ( s <= (g2 * g1) . t implies (d1 * d2) . s <= t ) & ( (d1 * d2) . s <= t implies s <= (g2 * g1) . t ) )
let s be Element of L3; :: thesis: for t being Element of L1 holds
( ( s <= (g2 * g1) . t implies (d1 * d2) . s <= t ) & ( (d1 * d2) . s <= t implies s <= (g2 * g1) . t ) )

let t be Element of L1; :: thesis: ( ( s <= (g2 * g1) . t implies (d1 * d2) . s <= t ) & ( (d1 * d2) . s <= t implies s <= (g2 * g1) . t ) )
s in the carrier of L3 ;
then A6: s in dom d2 by FUNCT_2:def 1;
t in the carrier of L1 ;
then A7: t in dom g1 by FUNCT_2:def 1;
thus ( s <= (g2 * g1) . t implies (d1 * d2) . s <= t ) :: thesis: ( (d1 * d2) . s <= t implies s <= (g2 * g1) . t )
proof
assume s <= (g2 * g1) . t ; :: thesis: (d1 * d2) . s <= t
then s <= g2 . (g1 . t) by ;
then d2 . s <= g1 . t by ;
then d1 . (d2 . s) <= d1 . (g1 . t) by A3;
then A8: d1 . (d2 . s) <= (d1 * g1) . t by ;
d1 * g1 <= id L1 by ;
then (d1 * g1) . t <= (id L1) . t by YELLOW_2:9;
then d1 . (d2 . s) <= (id L1) . t by ;
then d1 . (d2 . s) <= t ;
hence (d1 * d2) . s <= t by ; :: thesis: verum
end;
thus ( (d1 * d2) . s <= t implies s <= (g2 * g1) . t ) :: thesis: verum
proof
assume (d1 * d2) . s <= t ; :: thesis: s <= (g2 * g1) . t
then d1 . (d2 . s) <= t by ;
then d2 . s <= g1 . t by ;
then g2 . (d2 . s) <= g2 . (g1 . t) by A4;
then A9: (g2 * d2) . s <= g2 . (g1 . t) by ;
id L3 <= g2 * d2 by ;
then (id L3) . s <= (g2 * d2) . s by YELLOW_2:9;
then (id L3) . s <= g2 . (g1 . t) by ;
then s <= g2 . (g1 . t) ;
hence s <= (g2 * g1) . t by ; :: thesis: verum
end;
end;
d2 is monotone by ;
then A10: d1 * d2 is monotone by ;
g1 is monotone by ;
then g2 * g1 is monotone by ;
hence [(g2 * g1),(d1 * d2)] is Galois by ; :: thesis: verum