let R, T be non empty TopSpace; :: thesis: ( R is_Retract_of T iff ex S being non empty SubSpace of T st
( S is_a_retract_of T & S,R are_homeomorphic ) )
hereby :: thesis: ( ex S being non empty SubSpace of T st
( S is_a_retract_of T & S,R are_homeomorphic ) implies R is_Retract_of T )
assume R is_Retract_of T ; :: thesis: ex S being non empty SubSpace of T st
( S is_a_retract_of T & S,R are_homeomorphic )
then consider f being Function of T,T such that
A1: f is continuous and
A2: f * f = f and
A3: Image f,R are_homeomorphic by WAYBEL18:def 8;
reconsider S = Image f as non empty SubSpace of T ;
f = corestr f by WAYBEL18:def 7;
then reconsider f = f as continuous Function of T,S by A1, WAYBEL18:10;
take S = S; :: thesis: ( S is_a_retract_of T & S,R are_homeomorphic )
A4: [#] T = the carrier of T ;
[#] S = the carrier of S ;
then the carrier of S c= the carrier of T by A4, PRE_TOPC:def 4;
then reconsider rf = rng f as Subset of T by XBOOLE_1:1;
now :: thesis: for x being Point of T st x in the carrier of S holds
f . x = x
let x be Point of T; :: thesis: ( x in the carrier of S implies f . x = x )
assume x in the carrier of S ; :: thesis: f . x = x
then x in [#] (T | rf) by WAYBEL18:def 6;
then x in rng f by PRE_TOPC:def 5;
then ex y being object st
( y in dom f & x = f . y ) by FUNCT_1:def 3;
hence f . x = x by A2, FUNCT_1:13; :: thesis: verum
end;
then f is being_a_retraction ;
hence ( S is_a_retract_of T & S,R are_homeomorphic ) by A3; :: thesis: verum
end;
given S being non empty SubSpace of T such that A5: S is_a_retract_of T and
A6: S,R are_homeomorphic ; :: thesis: R is_Retract_of T
thus R is_Retract_of T by A5, A6, Th52, Th55; :: thesis: verum