let X be non empty discrete TopSpace; :: thesis: for X0 being non empty SubSpace of X ex r being continuous Function of X,X0 st r is being_a_retraction
let X0 be non empty SubSpace of X; :: thesis: ex r being continuous Function of X,X0 st r is being_a_retraction
reconsider A = the carrier of X0 as Subset of X by TSEP_1:1;
defpred S₁[ set , set ] means ( $1 in A implies $2 = $1 );
A1: for x being Point of X ex a being Point of X0 st S₁[x,a] ;
consider r being Function of X,X0 such that
A2: for x being Point of X holds S₁[x,r . x] from FUNCT_2:sch 3(A1);
reconsider r = r as continuous Function of X,X0 by Th62;
take r ; :: thesis: r is being_a_retraction
thus r is being_a_retraction by A2, BORSUK_1:def 16; :: thesis: verum