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 A1: f is_a_retraction_of T,S ; :: thesis: rng f = the carrier of S
then A2: f is Function of T,S by Def1;
f * (incl S,T) = id S by A1, Th10;
hence rng f = the carrier of S by A2, FUNCT_2:29; :: thesis: verum