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 :: thesis: for g being Element of (oContMaps (X,Y)) holds ((oContMaps (X,f)) * (oContMaps (X,f))) . g = (oContMaps (X,f)) . g

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:15
.= (oContMaps (X,f)) . (f * h) by Def2
.= f * (f * h) by Def2
.= (f * f) * h by RELAT_1:36
.= 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:63;
hence oContMaps (X,f) is idempotent by QUANTAL1:def 9; :: thesis: verum