let X be non empty TopSpace; :: thesis:
let x be Point of X; :: thesis:
let Y be monotone-convergence T_0-TopSpace; :: thesis:
set XY = oContMaps X,Y;
reconsider f = X --> x as continuous Function of X,X ;
set F = oContMaps f,Y;
dom f = the carrier of X by FUNCT_2:def 1;
then f * f = the carrier of X --> (f . x) by FUNCOP_1:23
.= f by FUNCOP_1:13 ;
then f is idempotent by QUANTAL1:def 9;
then oContMaps f,Y is idempotent directed-sups-preserving Function of (oContMaps X,Y),(oContMaps X,Y) by Th12, Th16;
then reconsider F = oContMaps f,Y as directed-sups-preserving projection Function of (oContMaps X,Y),(oContMaps X,Y) by WAYBEL_1:def 13;
take F ; :: thesis:

hereby :: thesis:

let h be continuous Function of X,Y; :: thesis:
A1: the carrier of X = dom h by FUNCT_2:def 1;
thus F . h = h * (the carrier of X --> x) by Def3
.= X --> (h . x) by A1, FUNCOP_1:23 ; :: thesis:

end;

thus ex h being continuous Function of X,X st
( h = X --> x & F = oContMaps h,Y ) ; :: thesis: