let J be non empty injective TopSpace; :: thesis: for Y being non empty TopSpace st J is SubSpace of Y holds
J is_Retract_of Y
let Y be non empty TopSpace; :: thesis: ( J is SubSpace of Y implies J is_Retract_of Y )
assume A1: J is SubSpace of Y ; :: thesis: J is_Retract_of Y
then consider f being Function of Y,J such that
A2: f is continuous and
A3: f | the carrier of J = id J by WAYBEL18:def 5;
A4: the carrier of J c= the carrier of Y by A1, BORSUK_1:1;
then reconsider ff = f as Function of Y,Y by FUNCT_2:7;
ex ff being Function of Y,Y st
( ff is continuous & ff * ff = ff & Image ff,J are_homeomorphic )

proof

reconsider M = [#] J as non empty Subset of Y by A1, BORSUK_1:1;
take ff ; :: thesis: ( ff is continuous & ff * ff = ff & Image ff,J are_homeomorphic )
thus ff is continuous by A1, A2, PRE_TOPC:26; :: thesis: ( ff * ff = ff & Image ff,J are_homeomorphic )
A5: dom f = the carrier of Y by FUNCT_2:def 1;
A6: for x being object st x in the carrier of Y holds
(f * f) . x = f . x

proof

let x be object ; :: thesis: ( x in the carrier of Y implies (f * f) . x = f . x )
assume A7: x in the carrier of Y ; :: thesis: (f * f) . x = f . x
hence (f * f) . x = f . (f . x) by A5, FUNCT_1:13
.= (id J) . (f . x) by A3, A7, FUNCT_1:49, FUNCT_2:5
.= f . x by A7, FUNCT_1:18, FUNCT_2:5 ;
:: thesis: verum

end;

dom (ff * ff) = the carrier of Y by FUNCT_2:def 1;
hence ff * ff = ff by A5, A6, FUNCT_1:2; :: thesis: Image ff,J are_homeomorphic
A8: rng f = the carrier of J

proof

thus rng f c= the carrier of J ; :: according to XBOOLE_0:def 10 :: thesis: the carrier of J c= rng f
let y be object ; :: according to TARSKI:def 3 :: thesis: ( not y in the carrier of J or y in rng f )
assume A9: y in the carrier of J ; :: thesis: y in rng f
then y in the carrier of Y by A4;
then A10: y in dom f by FUNCT_2:def 1;
f . y = (f | the carrier of J) . y by A9, FUNCT_1:49
.= y by A3, A9, FUNCT_1:18 ;
hence y in rng f by A10, FUNCT_1:def 3; :: thesis: verum

end;

the carrier of (Y | M) = [#] (Y | M)
.= the carrier of J by PRE_TOPC:def 5 ;
then Image ff = TopStruct(# the carrier of J, the topology of J #) by A1, A8, TSEP_1:5;
hence Image ff,J are_homeomorphic by YELLOW14:19; :: thesis: verum

end;

hence J is_Retract_of Y ; :: thesis: verum