thus ( X is_Retract_of Y implies ex c being continuous Function of X,Y ex r being continuous Function of Y,X st r * c = id X ) :: thesis:

proof

given f being Function of Y,Y such that A1: f is continuous and
A2: f * f = f and
A3: Image f,X are_homeomorphic ; :: according to WAYBEL18:def 8 :: thesis:
consider h being Function of (Image f),X such that
A4: h is being_homeomorphism by A3, T_0TOPSP:def 1;
h " is continuous by A4, TOPS_2:def 5;
then reconsider c = (incl (Image f)) * (h " ) as continuous Function of X,Y ;
( h is continuous & corestr f is continuous ) by A1, A4, TOPS_2:def 5, WAYBEL18:11;
then reconsider r = h * (corestr f) as continuous Function of Y,X ;
take c ; :: thesis:
take r ; :: thesis:
A5: ( rng h = [#] X & h is one-to-one ) by A4, TOPS_2:def 5;
thus r * c = h * ((corestr f) * ((incl (Image f)) * (h " ))) by RELAT_1:55
.= h * (((corestr f) * (incl (Image f))) * (h " )) by RELAT_1:55
.= h * ((id (Image f)) * (h " )) by A2, YELLOW14:36
.= h * (h " ) by FUNCT_2:23
.= id X by A5, TOPS_2:65 ; :: thesis:

end;

given c being continuous Function of X,Y, r being continuous Function of Y,X such that A6: r * c = id X ; :: thesis:
take f = c * r; :: according to WAYBEL18:def 8 :: thesis:
thus f is continuous ; :: thesis:
thus f * f = c * (r * (c * r)) by RELAT_1:55
.= c * ((id X) * r) by A6, RELAT_1:55
.= f by FUNCT_2:23 ; :: thesis:
dom c = the carrier of X by FUNCT_2:def 1
.= rng r by A6, FUNCT_2:24 ;
then A7: Image f = Image c by RELAT_1:47;
then reconsider cf = corestr c as Function of X,(Image f) ;
take h = cf " ; :: according to T_0TOPSP:def 1 :: thesis:
thus dom h = [#] (Image f) by FUNCT_2:def 1; :: according to TOPS_2:def 5 :: thesis:
A8: rng (corestr c) = [#] (Image c) by FUNCT_2:def 3;
A9: c is one-to-one by A6, FUNCT_2:29;
A10: corestr c is one-to-one by A6, FUNCT_2:29;
thus rng h = [#] X by A7, A8, A9, TOPS_2:62; :: thesis:
(corestr c) " is one-to-one by A9;
hence h is one-to-one by A7, A8, A9, TOPS_2:def 4; :: thesis:
A11: corestr c is continuous by WAYBEL18:11;
r * (cf * (cf " )) = (id X) * (cf " ) by A6, RELAT_1:55;
then r * (id the carrier of (Image c)) = (id X) * (cf " ) by A7, A8, A10, TOPS_2:65;
then A12: r * (id (Image c)) = cf " by FUNCT_2:23;
the carrier of (Image c) c= the carrier of Y by BORSUK_1:35;
then id (Image c) is Function of the carrier of (Image c),the carrier of Y by FUNCT_2:9;
then reconsider q = r * (id (Image c)) as Function of (Image f),X by A7;
A13: [#] X <> {} ;
for P being Subset of X st P is open holds
q " P is open

proof

let P be Subset of X; :: thesis:
assume A14: P is open ; :: thesis:
A15: q " P = (id (Image c)) " (r " P) by RELAT_1:181;
r " P is open by A13, A14, TOPS_2:55;
then A16: r " P in the topology of Y by PRE_TOPC:def 5;
A17: dom (id (Image c)) = [#] (Image c) by FUNCT_2:def 1;
(id (Image c)) " (r " P) = (r " P) /\ ([#] (Image c))

proof

thus (id (Image c)) " (r " P) c= (r " P) /\ ([#] (Image c)) :: according to XBOOLE_0:def 10 :: thesis:

proof

let a be set ; :: according to TARSKI:def 3 :: thesis:
assume A18: a in (id (Image c)) " (r " P) ; :: thesis:
then (id (Image c)) . a in r " P by FUNCT_1:def 13;
then a in r " P by A18, FUNCT_1:35;
hence a in (r " P) /\ ([#] (Image c)) by A18, XBOOLE_0:def 4; :: thesis:

end;

let a be set ; :: according to TARSKI:def 3 :: thesis:
assume A19: a in (r " P) /\ ([#] (Image c)) ; :: thesis:
then ( a in r " P & a in [#] (Image c) ) by XBOOLE_0:def 4;
then (id (Image c)) . a in r " P by FUNCT_1:35;
hence a in (id (Image c)) " (r " P) by A17, A19, FUNCT_1:def 13; :: thesis:

end;

hence q " P in the topology of (Image f) by A7, A15, A16, PRE_TOPC:def 9; :: according to PRE_TOPC:def 5 :: thesis:

end;

hence h is continuous by A12, A13, TOPS_2:55; :: thesis:
thus h " is continuous by A7, A8, A9, A11, TOPS_2:64; :: thesis: