let P, R be non empty Poset; for Con being Connection of P,R st Con is co-Galois holds
for f being Function of P,R
for g being Function of R,P st Con = [f,g] holds
( f = f * (g * f) & g = g * (f * g) )
let Con be Connection of P,R; ( Con is co-Galois implies for f being Function of P,R
for g being Function of R,P st Con = [f,g] holds
( f = f * (g * f) & g = g * (f * g) ) )
assume
Con is co-Galois
; for f being Function of P,R
for g being Function of R,P st Con = [f,g] holds
( f = f * (g * f) & g = g * (f * g) )
then consider f9 being Function of P,R, g9 being Function of R,P such that
A1:
Con = [f9,g9]
and
A2:
f9 is antitone
and
A3:
g9 is antitone
and
A4:
for p1, p2 being Element of P
for r1, r2 being Element of R holds
( p1 <= g9 . (f9 . p1) & r1 <= f9 . (g9 . r1) )
;
let f be Function of P,R; for g being Function of R,P st Con = [f,g] holds
( f = f * (g * f) & g = g * (f * g) )
let g be Function of R,P; ( Con = [f,g] implies ( f = f * (g * f) & g = g * (f * g) ) )
assume A5:
Con = [f,g]
; ( f = f * (g * f) & g = g * (f * g) )
A6: f =
[f,g] `1
.=
Con `1
by A5
.=
[f9,g9] `1
by A1
.=
f9
;
A7: g =
[f,g] `2
.=
Con `2
by A5
.=
[f9,g9] `2
by A1
.=
g9
;
A8:
dom g = the carrier of R
by FUNCT_2:def 1;
A9:
dom f = the carrier of P
by FUNCT_2:def 1;
A10:
for x being object st x in the carrier of P holds
f . x = (f * (g * f)) . x
proof
let x be
object ;
( x in the carrier of P implies f . x = (f * (g * f)) . x )
assume
x in the
carrier of
P
;
f . x = (f * (g * f)) . x
then reconsider x =
x as
Element of
P ;
x <= g . (f . x)
by A4, A6, A7;
then A11:
f . x >= f . (g . (f . x))
by A2, A6, WAYBEL_0:def 5;
f . x <= f . (g . (f . x))
by A4, A6, A7;
then
f . x = f . (g . (f . x))
by A11, ORDERS_2:2;
then A12:
f . x = f . ((g * f) . x)
by A9, FUNCT_1:13;
f . x is
Element of
R
;
then
x in dom (g * f)
by A9, A8, FUNCT_1:11;
hence
f . x = (f * (g * f)) . x
by A12, FUNCT_1:13;
verum
end;
A13:
for x being object st x in the carrier of R holds
g . x = (g * (f * g)) . x
proof
let x be
object ;
( x in the carrier of R implies g . x = (g * (f * g)) . x )
assume
x in the
carrier of
R
;
g . x = (g * (f * g)) . x
then reconsider x =
x as
Element of
R ;
x <= f . (g . x)
by A4, A6, A7;
then A14:
g . x >= g . (f . (g . x))
by A3, A7, WAYBEL_0:def 5;
g . x <= g . (f . (g . x))
by A4, A6, A7;
then
g . x = g . (f . (g . x))
by A14, ORDERS_2:2;
then A15:
g . x = g . ((f * g) . x)
by A8, FUNCT_1:13;
g . x is
Element of
P
;
then
x in dom (f * g)
by A9, A8, FUNCT_1:11;
hence
g . x = (g * (f * g)) . x
by A15, FUNCT_1:13;
verum
end;
( dom (f * (g * f)) = the carrier of P & dom (g * (f * g)) = the carrier of R )
by FUNCT_2:def 1;
hence
( f = f * (g * f) & g = g * (f * g) )
by A9, A8, A10, A13, FUNCT_1:2; verum