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

A6: now :: thesis: for x being object st x in the carrier of T holds
(f * f) . x = f . x

let x be object ; :: thesis: ( x in the carrier of T implies (f * f) . x = f . x )
assume A7: x in the carrier of T ; :: thesis: (f * f) . x = f . x
then A8: f . x in rng f by A4, FUNCT_1:def 3;
(f * f) . x = f . (f . x) by A4, A7, FUNCT_1:13;
hence (f * f) . x = f . x by A2, A5, A3, A8; :: thesis: verum

end;

dom (f * f) = the carrier of T by A5, A4, A3, RELAT_1:27;
then f * f = f by A4, A6, FUNCT_1:2;
hence f is idempotent by QUANTAL1:def 9; :: thesis: verum