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 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: ( ( 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) ) )

( h = X --> x & F = oContMaps (h,Y) ) ; :: thesis: verum

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 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: ( ( 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) )

thus
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:17 ; :: thesis: verum

end;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: verum

( h = X --> x & F = oContMaps (h,Y) ) ; :: thesis: verum