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;

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

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 ) )

d2 is monotone
by A2, WAYBEL_1:8;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 )

end;( ( 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

thus
( (d1 * d2) . s <= t implies s <= (g2 * g1) . t )
:: thesis: verum
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;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

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;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

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