let X be non empty almost_discrete TopSpace; :: thesis: for X0 being non empty discrete SubSpace of X ex r being continuous Function of X,X0 st r is being_a_retraction
let X0 be non empty discrete SubSpace of X; :: thesis: ex r being continuous Function of X,X0 st r is being_a_retraction
consider Z0 being non empty strict SubSpace of X such that
A1: X0 is SubSpace of Z0 and
A2: Z0 is maximal_discrete by Th61;
reconsider Z0 = Z0 as non empty strict maximal_discrete SubSpace of X by A2;
reconsider Z1 = Z0 as non empty TopSpace ;
reconsider Z1 = Z1 as non empty discrete TopSpace ;
reconsider X1 = X0 as non empty SubSpace of Z1 by A1;
consider g being continuous Function of Z1,X1 such that
A3: g is being_a_retraction by Th66;
reconsider g = g as continuous Function of Z0,X0 ;
consider h being continuous Function of X,Z0 such that
A4: h is being_a_retraction by Th68;
reconsider r = g * h as continuous Function of X,X0 ;
take r ; :: thesis: r is being_a_retraction
for x being Point of X st x in the carrier of X0 holds
r . x = x
proof
let x be Point of X; :: thesis: ( x in the carrier of X0 implies r . x = x )
assume A5: x in the carrier of X0 ; :: thesis: r . x = x
the carrier of X1 c= the carrier of Z1 by BORSUK_1:1;
then reconsider y = x as Point of Z1 by A5;
g . y = y by A3, A5, BORSUK_1:def 16;
then g . (h . x) = x by A4, BORSUK_1:def 16;
hence r . x = x by FUNCT_2:15; :: thesis: verum
end;
hence r is being_a_retraction by BORSUK_1:def 16; :: thesis: verum