let X be non empty TopSpace; :: thesis: ( InclPoset the topology of X is continuous implies for Y being injective T_0-TopSpace holds

( oContMaps (X,Y) is complete & oContMaps (X,Y) is continuous ) )

assume A1: InclPoset the topology of X is continuous ; :: thesis: for Y being injective T_0-TopSpace holds

( oContMaps (X,Y) is complete & oContMaps (X,Y) is continuous )

InclPoset the topology of X, oContMaps (X,Sierpinski_Space) are_isomorphic by Th6;

then reconsider XS = oContMaps (X,Sierpinski_Space) as non empty complete continuous Poset by A1, WAYBEL15:9, WAYBEL20:18;

let Y be injective T_0-TopSpace; :: thesis: ( oContMaps (X,Y) is complete & oContMaps (X,Y) is continuous )

consider M being non empty set such that

A2: Y is_Retract_of M -TOP_prod (M --> Sierpinski_Space) by WAYBEL18:19;

for i being Element of M holds (M --> Sierpinski_Space) . i is injective by FUNCOP_1:7;

then reconsider MS = M -TOP_prod (M --> Sierpinski_Space) as injective T_0-TopSpace by WAYBEL18:7;

for i being Element of M holds (M --> XS) . i is complete continuous LATTICE by FUNCOP_1:7;

then A3: ( M -POS_prod (M --> XS) is complete & M -POS_prod (M --> XS) is continuous ) by WAYBEL20:33;

M -POS_prod (M --> (oContMaps (X,Sierpinski_Space))), oContMaps (X,(M -TOP_prod (M --> Sierpinski_Space))) are_isomorphic by Th35, WAYBEL_1:6;

then ( oContMaps (X,MS) is complete & oContMaps (X,MS) is continuous ) by A3, WAYBEL15:9, WAYBEL20:18;

hence ( oContMaps (X,Y) is complete & oContMaps (X,Y) is continuous ) by A2, Th23; :: thesis: verum

( oContMaps (X,Y) is complete & oContMaps (X,Y) is continuous ) )

assume A1: InclPoset the topology of X is continuous ; :: thesis: for Y being injective T_0-TopSpace holds

( oContMaps (X,Y) is complete & oContMaps (X,Y) is continuous )

InclPoset the topology of X, oContMaps (X,Sierpinski_Space) are_isomorphic by Th6;

then reconsider XS = oContMaps (X,Sierpinski_Space) as non empty complete continuous Poset by A1, WAYBEL15:9, WAYBEL20:18;

let Y be injective T_0-TopSpace; :: thesis: ( oContMaps (X,Y) is complete & oContMaps (X,Y) is continuous )

consider M being non empty set such that

A2: Y is_Retract_of M -TOP_prod (M --> Sierpinski_Space) by WAYBEL18:19;

for i being Element of M holds (M --> Sierpinski_Space) . i is injective by FUNCOP_1:7;

then reconsider MS = M -TOP_prod (M --> Sierpinski_Space) as injective T_0-TopSpace by WAYBEL18:7;

for i being Element of M holds (M --> XS) . i is complete continuous LATTICE by FUNCOP_1:7;

then A3: ( M -POS_prod (M --> XS) is complete & M -POS_prod (M --> XS) is continuous ) by WAYBEL20:33;

M -POS_prod (M --> (oContMaps (X,Sierpinski_Space))), oContMaps (X,(M -TOP_prod (M --> Sierpinski_Space))) are_isomorphic by Th35, WAYBEL_1:6;

then ( oContMaps (X,MS) is complete & oContMaps (X,MS) is continuous ) by A3, WAYBEL15:9, WAYBEL20:18;

hence ( oContMaps (X,Y) is complete & oContMaps (X,Y) is continuous ) by A2, Th23; :: thesis: verum