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

now

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

end;

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