let T be non empty TopSpace; :: thesis: ( T is injective implies for S being non empty SubSpace of T st S is_a_retract_of T holds
S is injective )
assume A1: T is injective ; :: thesis: for S being non empty SubSpace of T st S is_a_retract_of T holds
S is injective
let S be non empty SubSpace of T; :: thesis: ( S is_a_retract_of T implies S is injective )
set p = incl S;
assume S is_a_retract_of T ; :: thesis: S is injective
then consider r being continuous Function of T,S such that
A2: r is being_a_retraction by BORSUK_1:def 17;
let X be non empty TopSpace; :: according to WAYBEL18:def 5 :: thesis: for f being Function of X,S st f is continuous holds
for Y being non empty TopSpace st X is SubSpace of Y holds
ex g being Function of Y,S st
( g is continuous & g | the carrier of X = f )
let F be Function of X,S; :: thesis: ( F is continuous implies for Y being non empty TopSpace st X is SubSpace of Y holds
ex g being Function of Y,S st
( g is continuous & g | the carrier of X = F ) )
assume A3: F is continuous ; :: thesis: for Y being non empty TopSpace st X is SubSpace of Y holds
ex g being Function of Y,S st
( g is continuous & g | the carrier of X = F )
reconsider f = (incl S) * F as Function of X,T ;
let Y be non empty TopSpace; :: thesis: ( X is SubSpace of Y implies ex g being Function of Y,S st
( g is continuous & g | the carrier of X = F ) )
assume A4: X is SubSpace of Y ; :: thesis: ex g being Function of Y,S st
( g is continuous & g | the carrier of X = F )
incl S is continuous by TMAP_1:87;
then consider g being Function of Y,T such that
A5: g is continuous and
A6: g | the carrier of X = f by A1, A3, A4;
take G = r * g; :: thesis: ( G is continuous & G | the carrier of X = F )
A7: the carrier of S c= the carrier of T by BORSUK_1:1;
A8: the carrier of X c= the carrier of Y by A4, BORSUK_1:1;
A9: for x being object st x in dom F holds
F . x = G . x

proof

let x be object ; :: thesis: ( x in dom F implies F . x = G . x )
assume A10: x in dom F ; :: thesis: F . x = G . x
then A11: ( x in the carrier of X & g . x = f . x ) by A6, FUNCT_1:49;
A12: F . x in rng F by A10, FUNCT_1:def 3;
then F . x in the carrier of S ;
then reconsider y = F . x as Point of T by A7;
A13: f . x = (incl S) . y by A10, FUNCT_2:15
.= F . x by A12, TMAP_1:84 ;
F . x = r . y by A2, A12, BORSUK_1:def 16;
hence F . x = G . x by A8, A13, A11, FUNCT_2:15; :: thesis: verum

end;

thus G is continuous by A5; :: thesis: G | the carrier of X = F
A14: dom F = the carrier of X by FUNCT_2:def 1;
(dom G) /\ the carrier of X = the carrier of Y /\ the carrier of X by FUNCT_2:def 1
.= the carrier of X by A4, BORSUK_1:1, XBOOLE_1:28 ;
hence G | the carrier of X = F by A14, A9, FUNCT_1:46; :: thesis: verum