let T, S be non empty Poset; :: thesis:
let f be monotone Function of T,S; :: thesis:
let g be monotone Function of S,T; :: thesis:
assume A1: f * g = id S ; :: thesis:
set h = g * f;
(g * f) * (g * f) = ((g * f) * g) * f by RELAT_1:36
.= (g * (id S)) * f by A1, RELAT_1:36
.= g * f by FUNCT_2:17 ;
then g * f is idempotent monotone Function of T,T by QUANTAL1:def 9, YELLOW_2:12;
then reconsider h = g * f as projection Function of T,T by WAYBEL_1:def 13;
A2: dom g = the carrier of S by FUNCT_2:def 1;
f is onto by A1, FUNCT_2:23;
then A3: rng f = the carrier of S by FUNCT_2:def 3;
then reconsider gg = corestr g as Function of S,(Image h) by A2, RELAT_1:28;
A4: gg = g by WAYBEL_1:30;

A5: now :: thesis:

let x, y be Element of S; :: thesis:
( x <= y implies ( g . x <= g . y & gg . x in the carrier of (Image h) ) ) by WAYBEL_1:def 2;
hence ( x <= y implies gg . x <= gg . y ) by A4, YELLOW_0:60; :: thesis:
(id S) . x = x ;
then A6: x = f . (g . x) by A1, FUNCT_2:15;
(id S) . y = y ;
then A7: y = f . (g . y) by A1, FUNCT_2:15;
assume gg . x <= gg . y ; :: thesis:
then g . x <= g . y by A4, YELLOW_0:59;
hence x <= y by A6, A7, WAYBEL_1:def 2; :: thesis:

end;

rng h = rng g by A3, A2, RELAT_1:28;
then A8: rng gg = the carrier of (Image h) by A4, YELLOW_0:def 15;
take h ; :: thesis:
thus h = g * f ; :: thesis:
thus h | the carrier of (Image h) = h * (inclusion h) by RELAT_1:65
.= (corestr h) * (inclusion h) by WAYBEL_1:30
.= id (Image h) by WAYBEL_1:33 ; :: thesis:
take gg ; :: according to WAYBEL_1:def 8 :: thesis:
gg is V7() by A1, A4, FUNCT_2:23;
hence gg is isomorphic by A8, A5, WAYBEL_0:66; :: thesis: