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 reconsider f = f as Function of T,S ;
f * (incl (S,T)) = id S by A1, Th7;
then f is onto by FUNCT_2:23;
hence rng f = the carrier of S by FUNCT_2:def 3; :: thesis: verum