theorem Th17: :: YELLOW16:18

for T, S being non empty Poset
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 )