let X be non empty TopSpace; :: thesis: for x being Point of X
for Y being monotone-convergence T_0-TopSpace ex F being directed-sups-preserving projection Function of (oContMaps (X,Y)),(oContMaps (X,Y)) st
( ( for f being continuous Function of X,Y holds F . f = X --> (f . x) ) & ex h being continuous Function of X,X st
( h = X --> x & F = oContMaps (h,Y) ) )

let x be Point of X; :: thesis: for Y being monotone-convergence T_0-TopSpace ex F being directed-sups-preserving projection Function of (oContMaps (X,Y)),(oContMaps (X,Y)) st
( ( for f being continuous Function of X,Y holds F . f = X --> (f . x) ) & ex h being continuous Function of X,X st
( h = X --> x & F = oContMaps (h,Y) ) )

let Y be monotone-convergence T_0-TopSpace; :: thesis: ex F being directed-sups-preserving projection Function of (oContMaps (X,Y)),(oContMaps (X,Y)) st
( ( for f being continuous Function of X,Y holds F . f = X --> (f . x) ) & ex h being continuous Function of X,X st
( h = X --> x & F = oContMaps (h,Y) ) )

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 ;
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: ( ( for f being continuous Function of X,Y holds F . f = X --> (f . x) ) & ex h being continuous Function of X,X st
( h = X --> x & F = oContMaps (h,Y) ) )

hereby :: thesis: ex h being continuous Function of X,X st
( h = X --> x & F = oContMaps (h,Y) )
let h be continuous Function of X,Y; :: thesis: F . h = X --> (h . x)
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 ; :: thesis: verum
end;
thus ex h being continuous Function of X,X st
( h = X --> x & F = oContMaps (h,Y) ) ; :: thesis: verum