let L1, L2 be non empty Poset; :: thesis: for f being Function of L1,L2

for f1 being Function of L2,L1 st f1 = f " & f is isomorphic holds

( [f,f1] is Galois & [f1,f] is Galois )

let f be Function of L1,L2; :: thesis: for f1 being Function of L2,L1 st f1 = f " & f is isomorphic holds

( [f,f1] is Galois & [f1,f] is Galois )

let f1 be Function of L2,L1; :: thesis: ( f1 = f " & f is isomorphic implies ( [f,f1] is Galois & [f1,f] is Galois ) )

assume that

A1: f1 = f " and

A2: f is isomorphic ; :: thesis: ( [f,f1] is Galois & [f1,f] is Galois )

A3: f1 is isomorphic by A1, A2, WAYBEL_0:68;

for f1 being Function of L2,L1 st f1 = f " & f is isomorphic holds

( [f,f1] is Galois & [f1,f] is Galois )

let f be Function of L1,L2; :: thesis: for f1 being Function of L2,L1 st f1 = f " & f is isomorphic holds

( [f,f1] is Galois & [f1,f] is Galois )

let f1 be Function of L2,L1; :: thesis: ( f1 = f " & f is isomorphic implies ( [f,f1] is Galois & [f1,f] is Galois ) )

assume that

A1: f1 = f " and

A2: f is isomorphic ; :: thesis: ( [f,f1] is Galois & [f1,f] is Galois )

A3: f1 is isomorphic by A1, A2, WAYBEL_0:68;

now :: thesis: for t being Element of L2

for s being Element of L1 holds

( ( t <= f . s implies f1 . t <= s ) & ( f1 . t <= s implies t <= f . s ) )

hence
[f,f1] is Galois
by A2, A3; :: thesis: [f1,f] is Galois for s being Element of L1 holds

( ( t <= f . s implies f1 . t <= s ) & ( f1 . t <= s implies t <= f . s ) )

let t be Element of L2; :: thesis: for s being Element of L1 holds

( ( t <= f . s implies f1 . t <= s ) & ( f1 . t <= s implies t <= f . s ) )

let s be Element of L1; :: thesis: ( ( t <= f . s implies f1 . t <= s ) & ( f1 . t <= s implies t <= f . s ) )

s in the carrier of L1 ;

then A4: s in dom f by FUNCT_2:def 1;

A5: f1 * f = id (dom f) by A1, A2, FUNCT_1:39

.= id L1 by FUNCT_2:def 1 ;

thus ( t <= f . s implies f1 . t <= s ) :: thesis: ( f1 . t <= s implies t <= f . s )

then A6: t in dom f1 by FUNCT_2:def 1;

A7: f * f1 = id (rng f) by A1, A2, FUNCT_1:39

.= id L2 by A2, WAYBEL_0:66 ;

thus ( f1 . t <= s implies t <= f . s ) :: thesis: verum

end;( ( t <= f . s implies f1 . t <= s ) & ( f1 . t <= s implies t <= f . s ) )

let s be Element of L1; :: thesis: ( ( t <= f . s implies f1 . t <= s ) & ( f1 . t <= s implies t <= f . s ) )

s in the carrier of L1 ;

then A4: s in dom f by FUNCT_2:def 1;

A5: f1 * f = id (dom f) by A1, A2, FUNCT_1:39

.= id L1 by FUNCT_2:def 1 ;

thus ( t <= f . s implies f1 . t <= s ) :: thesis: ( f1 . t <= s implies t <= f . s )

proof

t in the carrier of L2
;
assume
t <= f . s
; :: thesis: f1 . t <= s

then f1 . t <= f1 . (f . s) by A3, WAYBEL_1:def 2;

then f1 . t <= (f1 * f) . s by A4, FUNCT_1:13;

hence f1 . t <= s by A5; :: thesis: verum

end;then f1 . t <= f1 . (f . s) by A3, WAYBEL_1:def 2;

then f1 . t <= (f1 * f) . s by A4, FUNCT_1:13;

hence f1 . t <= s by A5; :: thesis: verum

then A6: t in dom f1 by FUNCT_2:def 1;

A7: f * f1 = id (rng f) by A1, A2, FUNCT_1:39

.= id L2 by A2, WAYBEL_0:66 ;

thus ( f1 . t <= s implies t <= f . s ) :: thesis: verum

now :: thesis: for t being Element of L1

for s being Element of L2 holds

( ( t <= f1 . s implies f . t <= s ) & ( f . t <= s implies t <= f1 . s ) )

hence
[f1,f] is Galois
by A2, A3; :: thesis: verumfor s being Element of L2 holds

( ( t <= f1 . s implies f . t <= s ) & ( f . t <= s implies t <= f1 . s ) )

let t be Element of L1; :: thesis: for s being Element of L2 holds

( ( t <= f1 . s implies f . t <= s ) & ( f . t <= s implies t <= f1 . s ) )

let s be Element of L2; :: thesis: ( ( t <= f1 . s implies f . t <= s ) & ( f . t <= s implies t <= f1 . s ) )

s in the carrier of L2 ;

then A8: s in dom f1 by FUNCT_2:def 1;

A9: f * f1 = id (rng f) by A1, A2, FUNCT_1:39

.= id L2 by A2, WAYBEL_0:66 ;

thus ( t <= f1 . s implies f . t <= s ) :: thesis: ( f . t <= s implies t <= f1 . s )

then A10: t in dom f by FUNCT_2:def 1;

A11: f1 * f = id (dom f) by A1, A2, FUNCT_1:39

.= id L1 by FUNCT_2:def 1 ;

thus ( f . t <= s implies t <= f1 . s ) :: thesis: verum

end;( ( t <= f1 . s implies f . t <= s ) & ( f . t <= s implies t <= f1 . s ) )

let s be Element of L2; :: thesis: ( ( t <= f1 . s implies f . t <= s ) & ( f . t <= s implies t <= f1 . s ) )

s in the carrier of L2 ;

then A8: s in dom f1 by FUNCT_2:def 1;

A9: f * f1 = id (rng f) by A1, A2, FUNCT_1:39

.= id L2 by A2, WAYBEL_0:66 ;

thus ( t <= f1 . s implies f . t <= s ) :: thesis: ( f . t <= s implies t <= f1 . s )

proof

t in the carrier of L1
;
assume
t <= f1 . s
; :: thesis: f . t <= s

then f . t <= f . (f1 . s) by A2, WAYBEL_1:def 2;

then f . t <= (f * f1) . s by A8, FUNCT_1:13;

hence f . t <= s by A9; :: thesis: verum

end;then f . t <= f . (f1 . s) by A2, WAYBEL_1:def 2;

then f . t <= (f * f1) . s by A8, FUNCT_1:13;

hence f . t <= s by A9; :: thesis: verum

then A10: t in dom f by FUNCT_2:def 1;

A11: f1 * f = id (dom f) by A1, A2, FUNCT_1:39

.= id L1 by FUNCT_2:def 1 ;

thus ( f . t <= s implies t <= f1 . s ) :: thesis: verum