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:35;
then reconsider ff = f as Function of Y,Y by FUNCT_2:9;
ex ff being Function of Y,Y st
( ff is continuous & ff * ff = ff & Image ff,J are_homeomorphic )
proof
take
ff
;
:: thesis: ( ff is continuous & ff * ff = ff & Image ff,J are_homeomorphic )
thus
ff is
continuous
by A1, A2, PRE_TOPC:56;
:: thesis: ( ff * ff = ff & Image ff,J are_homeomorphic )
A5:
dom (ff * ff) = the
carrier of
Y
by FUNCT_2:def 1;
A6:
dom f = the
carrier of
Y
by FUNCT_2:def 1;
for
x being
set st
x in the
carrier of
Y holds
(f * f) . x = f . x
hence
ff * ff = ff
by A5, A6, FUNCT_1:9;
:: thesis: Image ff,J are_homeomorphic
A8:
rng f = the
carrier of
J
reconsider M =
[#] J as non
empty Subset of
Y by A1, BORSUK_1:35;
the
carrier of
(Y | M) =
[#] (Y | M)
.=
the
carrier of
J
by PRE_TOPC:def 10
;
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:20;
:: thesis: verum
end;
hence
J is_Retract_of Y
by WAYBEL18:def 8; :: thesis: verum