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

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