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: ( g1 is monotone & d1 is monotone ) by A1, WAYBEL_1:9;
A4: ( g2 is monotone & d2 is monotone ) by A2, WAYBEL_1:9;
then A5: g2 * g1 is monotone by A3, YELLOW_2:14;
A6: d1 * d2 is monotone by A3, A4, YELLOW_2:14;

now

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 ) )
( g1 is Function of the carrier of L1,the carrier of L2 & t in the carrier of L1 ) ;
then A7: t in dom g1 by FUNCT_2:def 1;
( d2 is Function of the carrier of L3,the carrier of L2 & s in the carrier of L3 ) ;
then A8: s in dom d2 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

d1 * g1 <= id L1 by A1, WAYBEL_1:19;
then A9: (d1 * g1) . t <= (id L1) . t by YELLOW_2:10;
assume s <= (g2 * g1) . t ; :: thesis: (d1 * d2) . s <= t
then s <= g2 . (g1 . t) by A7, FUNCT_1:23;
then d2 . s <= g1 . t by A2, WAYBEL_1:9;
then d1 . (d2 . s) <= d1 . (g1 . t) by A3, WAYBEL_1:def 2;
then d1 . (d2 . s) <= (d1 * g1) . t by A7, FUNCT_1:23;
then d1 . (d2 . s) <= (id L1) . t by A9, ORDERS_2:26;
then d1 . (d2 . s) <= t by FUNCT_1:35;
hence (d1 * d2) . s <= t by A8, FUNCT_1:23; :: thesis: verum

end;

thus ( (d1 * d2) . s <= t implies s <= (g2 * g1) . t ) :: thesis: verum

proof

id L3 <= g2 * d2 by A2, WAYBEL_1:19;
then A10: (id L3) . s <= (g2 * d2) . s by YELLOW_2:10;
assume (d1 * d2) . s <= t ; :: thesis: s <= (g2 * g1) . t
then d1 . (d2 . s) <= t by A8, FUNCT_1:23;
then d2 . s <= g1 . t by A1, WAYBEL_1:9;
then g2 . (d2 . s) <= g2 . (g1 . t) by A4, WAYBEL_1:def 2;
then (g2 * d2) . s <= g2 . (g1 . t) by A8, FUNCT_1:23;
then (id L3) . s <= g2 . (g1 . t) by A10, ORDERS_2:26;
then s <= g2 . (g1 . t) by FUNCT_1:35;
hence s <= (g2 * g1) . t by A7, FUNCT_1:23; :: thesis: verum

end;

end;

hence [(g2 * g1),(d1 * d2)] is Galois by A5, A6, WAYBEL_1:9; :: thesis: verum