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:55
.= (g * (id S)) * f by A1, RELAT_1:55
.= g * f by FUNCT_2:23 ;
then g * f is idempotent monotone Function of T,T by QUANTAL1:def 9, YELLOW_2:14;
then reconsider h = g * f as projection Function of T,T by WAYBEL_1:def 13;
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:94
.= (corestr h) * (inclusion h) by WAYBEL_1:32
.= id (Image h) by WAYBEL_1:36 ; :: thesis: S, Image h are_isomorphic
( rng f = the carrier of S & dom g = the carrier of S ) by A1, FUNCT_2:29, FUNCT_2:def 1;
then A2: rng h = rng g by RELAT_1:47;
then reconsider gg = corestr g as Function of S,(Image h) ;
take gg ; :: according to WAYBEL_1:def 8 :: thesis: gg is isomorphic
A3: gg = g by WAYBEL_1:32;
then A4: gg is one-to-one by A1, FUNCT_2:29;
A5: rng gg = the carrier of (Image h) by A2, A3, YELLOW_0:def 15;

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 A3, YELLOW_0:61; :: thesis: ( gg . x <= gg . y implies x <= y )
assume gg . x <= gg . y ; :: thesis: x <= y
then A6: g . x <= g . y by A3, YELLOW_0:60;
( (id S) . x = x & (id S) . y = y ) by FUNCT_1:35;
then ( x = f . (g . x) & y = f . (g . y) ) by A1, FUNCT_2:21;
hence x <= y by A6, WAYBEL_1:def 2; :: thesis: verum

end;

hence gg is isomorphic by A4, A5, WAYBEL_0:66; :: thesis: verum