let X be non empty TopSpace; :: thesis: for Y being monotone-convergence T_0-TopSpace st oContMaps (X,Y) is complete & oContMaps (X,Y) is continuous holds
( Omega Y is complete & Omega Y is continuous )
let Y be monotone-convergence T_0-TopSpace; :: thesis: ( oContMaps (X,Y) is complete & oContMaps (X,Y) is continuous implies ( Omega Y is complete & Omega Y is continuous ) )
assume A1: ( oContMaps (X,Y) is complete & oContMaps (X,Y) is continuous ) ; :: thesis: ( Omega Y is complete & Omega Y is continuous )
set b = the Element of X;
A2: TopStruct(# the carrier of (Omega Y), the topology of (Omega Y) #) = TopStruct(# the carrier of Y, the topology of Y #) by WAYBEL25:def 2;
consider F being directed-sups-preserving projection Function of (oContMaps (X,Y)),(oContMaps (X,Y)) such that
A3: for f being continuous Function of X,Y holds F . f = X --> (f . the Element of X) and
ex h being continuous Function of X,X st
( h = X --> the Element of X & F = oContMaps (h,Y) ) by Th27;
oContMaps (X,Y) is full SubRelStr of (Omega Y) |^ the carrier of X by WAYBEL24:def 3;
then reconsider imF = Image F as non empty full SubRelStr of (Omega Y) |^ the carrier of X by YELLOW16:26;
A4: the carrier of imF = rng F by YELLOW_0:def 15;
A5: dom F = the carrier of (oContMaps (X,Y)) by FUNCT_2:52;

now :: thesis: for a being set holds
( ( a is Element of imF implies ex x being Element of (Omega Y) st a = the carrier of X --> x ) & ( ex x being Element of (Omega Y) st a = the carrier of X --> x implies a is Element of imF ) )

let a be set ; :: thesis: ( ( a is Element of imF implies ex x being Element of (Omega Y) st a = the carrier of X --> x ) & ( ex x being Element of (Omega Y) st a = the carrier of X --> x implies a is Element of imF ) )

hereby :: thesis: ( ex x being Element of (Omega Y) st a = the carrier of X --> x implies a is Element of imF )

assume a is Element of imF ; :: thesis: ex x being Element of (Omega Y) st a = the carrier of X --> x
then consider h being object such that
A6: h in dom F and
A7: a = F . h by A4, FUNCT_1:def 3;
reconsider h = h as continuous Function of X,Y by A6, Th2;
reconsider x = h . the Element of X as Element of (Omega Y) by A2;
a = X --> (h . the Element of X) by A3, A7
.= the carrier of X --> x ;
hence ex x being Element of (Omega Y) st a = the carrier of X --> x ; :: thesis: verum

end;

given x being Element of (Omega Y) such that A8: a = the carrier of X --> x ; :: thesis: a is Element of imF
a = X --> x by A8;
then A9: a is Element of (oContMaps (X,Y)) by Th1;
then reconsider h = a as continuous Function of X,Y by Th2;
A10: X --> (h . the Element of X) = the carrier of X --> (h . the Element of X) ;
h . the Element of X = x by A8, FUNCOP_1:7;
then F . a = X --> x by A3, A10;
hence a is Element of imF by A4, A5, A8, A9, FUNCT_1:def 3; :: thesis: verum

end;

then Omega Y,imF are_isomorphic by YELLOW16:50;
then A11: imF, Omega Y are_isomorphic by WAYBEL_1:6;
Image F is complete continuous LATTICE by A1, WAYBEL15:15, YELLOW_2:35;
hence ( Omega Y is complete & Omega Y is continuous ) by A11, WAYBEL15:9, WAYBEL20:18; :: thesis: verum