let T be non empty TopSpace; :: thesis: for S being non empty SubSpace of T
for f being Function of T,S st f is being_a_retraction holds
rng f = the carrier of S
let S be non empty SubSpace of T; :: thesis: for f being Function of T,S st f is being_a_retraction holds
rng f = the carrier of S
let f be Function of T,S; :: thesis: ( f is being_a_retraction implies rng f = the carrier of S )
assume A1: for W being Point of T st W in the carrier of S holds
f . W = W ; :: according to BORSUK_1:def 19 :: thesis: rng f = the carrier of S
thus rng f c= the carrier of S ; :: according to XBOOLE_0:def 10 :: thesis: the carrier of S c= rng f
( [#] T = the carrier of T & [#] S = the carrier of S ) ;
then A2: the carrier of S c= the carrier of T by PRE_TOPC:def 9;
let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in the carrier of S or x in rng f )
assume A3: x in the carrier of S ; :: thesis: x in rng f
then x in the carrier of T by A2;
then ( f . x = x & x in dom f ) by A1, A3, FUNCT_2:def 1;
hence x in rng f by FUNCT_1:def 5; :: thesis: verum