let J be non empty injective TopSpace; for Y being non empty TopSpace st J is SubSpace of Y holds
J is_Retract_of Y
let Y be non empty TopSpace; ( J is SubSpace of Y implies J is_Retract_of Y )
assume A1:
J is SubSpace of Y
; 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
;
( ff is continuous & ff * ff = ff & Image ff,J are_homeomorphic )
thus
ff is
continuous
by A1, A2, PRE_TOPC:26;
( 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
dom (ff * ff) = the
carrier of
Y
by FUNCT_2:def 1;
hence
ff * ff = ff
by A5, A6, FUNCT_1:2;
Image ff,J are_homeomorphic
A8:
rng f = the
carrier of
J
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;
verum
end;
hence
J is_Retract_of Y
; verum