let T, S be non empty Poset; :: thesis: for f being monotone Function of T,S
for g being monotone Function of S,T st f * g = id S holds
ex h being projection Function of T,T st
( h = g * f & h | the carrier of (Image h) = id (Image h) & S, Image h are_isomorphic )
let f be monotone Function of T,S; :: thesis: for g being monotone Function of S,T st f * g = id S holds
ex h being projection Function of T,T st
( h = g * f & h | the carrier of (Image h) = id (Image h) & S, Image h are_isomorphic )
let g be monotone Function of S,T; :: thesis: ( f * g = id S implies ex h being projection Function of T,T st
( h = g * f & h | the carrier of (Image h) = id (Image h) & S, Image h are_isomorphic ) )
assume A1: f * g = id S ; :: thesis: ex h being projection Function of T,T st
( h = g * f & h | the carrier of (Image h) = id (Image h) & S, Image h are_isomorphic )
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

let x, y be Element of S; :: thesis: ( ( x <= y implies gg . x <= gg . y ) & ( gg . x <= gg . y implies x <= y ) )
( 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: ( gg . x <= gg . y implies x <= y )
(id S) . x = x by FUNCT_1:18;
then A6: x = f . (g . x) by A1, FUNCT_2:15;
(id S) . y = y by FUNCT_1:18;
then A7: y = f . (g . y) by A1, FUNCT_2:15;
assume gg . x <= gg . y ; :: thesis: x <= y
then g . x <= g . y by A4, YELLOW_0:59;
hence x <= y by A6, A7, WAYBEL_1:def 2; :: thesis: verum

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: ( h = g * f & h | the carrier of (Image h) = id (Image h) & S, Image h are_isomorphic )
thus h = g * f ; :: thesis: ( h | the carrier of (Image h) = id (Image h) & S, Image h are_isomorphic )
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: S, Image h are_isomorphic
take gg ; :: according to WAYBEL_1:def 8 :: thesis: gg is isomorphic
gg is one-to-one by A1, A4, FUNCT_2:23;
hence gg is isomorphic by A8, A5, WAYBEL_0:66; :: thesis: verum