let X, Y be non empty TopSpace; :: thesis: for f being continuous Function of Y,Y st f is idempotent holds
oContMaps X,f is idempotent
let f be continuous Function of Y,Y; :: thesis: ( f is idempotent implies oContMaps X,f is idempotent )
assume A1: f is idempotent ; :: thesis: oContMaps X,f is idempotent
set Xf = oContMaps X,f;

now

let g be Element of (oContMaps X,Y); :: thesis: ((oContMaps X,f) * (oContMaps X,f)) . g = (oContMaps X,f) . g
reconsider h = g as continuous Function of X,Y by Th2;
thus ((oContMaps X,f) * (oContMaps X,f)) . g = (oContMaps X,f) . ((oContMaps X,f) . g) by FUNCT_2:21
.= (oContMaps X,f) . (f * h) by Def2
.= f * (f * h) by Def2
.= (f * f) * h by RELAT_1:55
.= f * h by A1, QUANTAL1:def 9
.= (oContMaps X,f) . g by Def2 ; :: thesis: verum

end;

then (oContMaps X,f) * (oContMaps X,f) = oContMaps X,f by FUNCT_2:113;
hence oContMaps X,f is idempotent by QUANTAL1:def 9; :: thesis: verum