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 16 :: 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
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in the carrier of S or x in rng f )
A2: [#] S = the carrier of S ;
[#] T = the carrier of T ;
then A3: the carrier of S c= the carrier of T by A2, PRE_TOPC:def 4;
assume A4: x in the carrier of S ; :: thesis: x in rng f
then x in the carrier of T by A3;
then A5: x in dom f by FUNCT_2:def 1;
f . x = x by A1, A3, A4;
hence x in rng f by A5, FUNCT_1:def 3; :: thesis: verum