let T be non empty TopSpace; :: thesis: for S being non empty SubSpace of T
for f being continuous Function of T,S st f is being_a_retraction holds
f * (incl S,T) = id S
let S be non empty SubSpace of T; :: thesis: for f being continuous Function of T,S st f is being_a_retraction holds
f * (incl S,T) = id S
let f be continuous Function of T,S; :: thesis: ( f is being_a_retraction implies f * (incl S,T) = id S )
assume A1: f is being_a_retraction ; :: thesis: f * (incl S,T) = id S
( [#] 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;
then A3: incl S,T = id the carrier of S by YELLOW_9:def 1;

now

let x be Element of S; :: thesis: (f * (incl S,T)) . x = (id S) . x
x in the carrier of S ;
then reconsider y = x as Point of T by A2;
thus (f * (incl S,T)) . x = f . ((incl S,T) . x) by FUNCT_2:21
.= f . x by A3, FUNCT_1:35
.= y by A1, BORSUK_1:def 19
.= (id S) . x by FUNCT_1:35 ; :: thesis: verum

end;

hence f * (incl S,T) = id S by FUNCT_2:113; :: thesis: verum