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);

hence oContMaps (X,f) is idempotent by QUANTAL1:def 9; :: thesis: verum

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

then
(oContMaps (X,f)) * (oContMaps (X,f)) = oContMaps (X,f)
by FUNCT_2:63;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;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

hence oContMaps (X,f) is idempotent by QUANTAL1:def 9; :: thesis: verum