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 )
consider b being 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 . b) and
ex h being continuous Function of X,X st
( h = X --> b & F = oContMaps h,Y ) by Th28;
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:28;
A4: the carrier of imF = rng F by YELLOW_0:def 15;
A5: dom F = the carrier of (oContMaps X,Y) by FUNCT_2:67;

now

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 set such that
A6: h in dom F and
A7: a = F . h by A4, FUNCT_1:def 5;
reconsider h = h as continuous Function of X,Y by A6, Th2;
reconsider x = h . b as Element of (Omega Y) by A2;
a = X --> (h . b) 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 . b) = the carrier of X --> (h . b) ;
h . b = x by A8, FUNCOP_1:13;
then F . a = X --> x by A3, A10;
hence a is Element of imF by A4, A5, A8, A9, FUNCT_1:def 5; :: thesis: verum

end;

then Omega Y,imF are_isomorphic by YELLOW16:52;
then A11: imF, Omega Y are_isomorphic by WAYBEL_1:7;
Image F is complete continuous LATTICE by A1, WAYBEL15:17, YELLOW_2:37;
hence ( Omega Y is complete & Omega Y is continuous ) by A11, WAYBEL15:11, WAYBEL20:18; :: thesis: verum