let T, S be non empty Poset; :: thesis: for f being Function of T,T st f is_a_retraction_of T,S holds
Image f = RelStr(# the carrier of S,the InternalRel of S #)
let f be Function of T,T; :: thesis: ( f is_a_retraction_of T,S implies Image f = RelStr(# the carrier of S,the InternalRel of S #) )
assume f is_a_retraction_of T,S ; :: thesis: Image f = RelStr(# the carrier of S,the InternalRel of S #)
then A1: ( rng f = the carrier of S & S is full SubRelStr of T ) by Def1, Th12;
the carrier of (Image f) = rng f by YELLOW_0:def 15;
hence Image f = RelStr(# the carrier of S,the InternalRel of S #) by A1, YELLOW_0:58; :: thesis: verum