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: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: ( ( 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 A1, FUNCOP_1:23 ; :: thesis: verum

end;

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