let T, S, R be non empty TopSpace; :: thesis: ( S is_Retract_of T & S,R are_homeomorphic implies R is_Retract_of T )
given f being continuous Function of S,T, g being continuous Function of T,S such that A1: g * f = id S ; :: according to WAYBEL25:def 1 :: thesis: ( not S,R are_homeomorphic or R is_Retract_of T )
given h being Function of S,R such that A2: h is being_homeomorphism ; :: according to T_0TOPSP:def 1 :: thesis: R is_Retract_of T
h " is continuous by A2, TOPS_2:def 5;
then reconsider f9 = f * (h ") as continuous Function of R,T ;
h is continuous by A2, TOPS_2:def 5;
then reconsider g9 = h * g as continuous Function of T,R ;
take f9 ; :: according to WAYBEL25:def 1 :: thesis: ex b₁ being Element of bool [: the carrier of T, the carrier of R:] st b₁ * f9 = id R
take g9 ; :: thesis: g9 * f9 = id R
thus g9 * f9 = id R by A1, A2, Th51; :: thesis: verum