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 is idempotent
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 is idempotent
let f be continuous Function of T,S; :: thesis: ( f is being_a_retraction implies f is idempotent )
assume A1: f is being_a_retraction ; :: thesis: f is idempotent
( [#] 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;
A3: ( dom f = the carrier of T & rng f = the carrier of S ) by A1, Th46, FUNCT_2:def 1;
then A4: dom (f * f) = the carrier of T by A2, RELAT_1:46;

now

let x be set ; :: thesis: ( x in the carrier of T implies (f * f) . x = f . x )
assume x in the carrier of T ; :: thesis: (f * f) . x = f . x
then ( (f * f) . x = f . (f . x) & f . x in rng f ) by A3, FUNCT_1:23, FUNCT_1:def 5;
hence (f * f) . x = f . x by A1, A2, A3, BORSUK_1:def 19; :: thesis: verum

end;

then f * f = f by A3, A4, FUNCT_1:9;
hence f is idempotent by QUANTAL1:def 9; :: thesis: verum