let T be non empty TopSpace; 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; 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; ( f is being_a_retraction implies f is idempotent )
assume A2:
f is being_a_retraction
; 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;
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; verum