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:17
.= f by FUNCOP_1:7 ;
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 Th11, Th15;
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:17 ; :: thesis:

end;

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