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