let S, T be non empty TopSpace; :: thesis: ( T is injective & S is_Retract_of T implies S is injective )
assume that
A1: T is injective and
A2: S is_Retract_of T ; :: thesis: S is injective
consider h being Function of T,T such that
A3: h is continuous and
A4: h * h = h and
A5: Image h,S are_homeomorphic by A2;
set F = corestr h;
for W being Point of T st W in the carrier of (Image h) holds
(corestr h) . W = W
proof
let W be Point of T; :: thesis: ( W in the carrier of (Image h) implies (corestr h) . W = W )
assume W in the carrier of (Image h) ; :: thesis: (corestr h) . W = W
then W in rng h by WAYBEL18:9;
then ex x being object st
( x in dom h & W = h . x ) by FUNCT_1:def 3;
hence (corestr h) . W = W by A4, FUNCT_1:13; :: thesis: verum
end;
then A6: corestr h is being_a_retraction by BORSUK_1:def 16;
corestr h is continuous by A3, WAYBEL18:10;
then Image h is_a_retract_of T by A6, BORSUK_1:def 17;
then Image h is injective by A1, WAYBEL18:8;
hence S is injective by A5, Th6; :: thesis: verum