let P, R be non empty Poset; :: thesis: 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; :: thesis: ( 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 ; :: thesis: 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; :: thesis: 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; :: thesis: ( Con = [f,g] implies ( f = f * (g * f) & g = g * (f * g) ) )
assume A5: Con = [f,g] ; :: thesis: ( 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 ; :: thesis: ( x in the carrier of P implies f . x = (f * (g * f)) . x )
assume x in the carrier of P ; :: thesis: 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; :: thesis: 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 ; :: thesis: ( x in the carrier of R implies g . x = (g * (f * g)) . x )
assume x in the carrier of R ; :: thesis: 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; :: thesis: 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; :: thesis: verum