let S, T be non empty Poset; :: thesis: for f being Function st f is_a_retraction_of T,S holds
rng f = the carrier of S
let f be Function; :: thesis: ( f is_a_retraction_of T,S implies rng f = the carrier of S )
assume f is_a_retraction_of T,S ; :: thesis: rng f = the carrier of S
then ( f * (incl S,T) = id S & f is Function of T,S ) by Def1, Th10;
hence rng f = the carrier of S by FUNCT_2:29; :: thesis: verum