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 A1, WAYBEL_1:8;
A4: g2 is monotone by A2, WAYBEL_1:8;

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 A7, FUNCT_1:13;
then d2 . s <= g1 . t by A2, WAYBEL_1:8;
then d1 . (d2 . s) <= d1 . (g1 . t) by A3;
then A8: d1 . (d2 . s) <= (d1 * g1) . t by A7, FUNCT_1:13;
d1 * g1 <= id L1 by A1, WAYBEL_1:18;
then (d1 * g1) . t <= (id L1) . t by YELLOW_2:9;
then d1 . (d2 . s) <= (id L1) . t by A8, ORDERS_2:3;
then d1 . (d2 . s) <= t ;
hence (d1 * d2) . s <= t by A6, FUNCT_1:13; :: 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 A6, FUNCT_1:13;
then d2 . s <= g1 . t by A1, WAYBEL_1:8;
then g2 . (d2 . s) <= g2 . (g1 . t) by A4;
then A9: (g2 * d2) . s <= g2 . (g1 . t) by A6, FUNCT_1:13;
id L3 <= g2 * d2 by A2, WAYBEL_1:18;
then (id L3) . s <= (g2 * d2) . s by YELLOW_2:9;
then (id L3) . s <= g2 . (g1 . t) by A9, ORDERS_2:3;
then s <= g2 . (g1 . t) ;
hence s <= (g2 * g1) . t by A7, FUNCT_1:13; :: thesis: verum

end;

end;

d2 is monotone by A2, WAYBEL_1:8;
then A10: d1 * d2 is monotone by A3, YELLOW_2:12;
g1 is monotone by A1, WAYBEL_1:8;
then g2 * g1 is monotone by A4, YELLOW_2:12;
hence [(g2 * g1),(d1 * d2)] is Galois by A10, A5; :: thesis: verum