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
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;
then A4: incl (S,T) = id the carrier of S by YELLOW_9:def 1;

now :: thesis: for x being Element of S holds (f * (incl (S,T))) . x = (id S) . x

let x be Element of S; :: thesis: (f * (incl (S,T))) . x = (id S) . x
reconsider y = x as Point of T by A3;
thus (f * (incl (S,T))) . x = f . ((incl (S,T)) . x) by FUNCT_2:15
.= f . x by A4
.= y by A1
.= (id S) . x ; :: thesis: verum

end;

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