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:11, 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:20;
for i being Element of M holds (M --> Sierpinski_Space ) . i is injective by FUNCOP_1:13;
then reconsider MS = M -TOP_prod (M --> Sierpinski_Space ) as injective T_0-TopSpace by WAYBEL18:8;
for i being Element of M holds (M --> XS) . i is complete continuous LATTICE by FUNCOP_1:13;
then A3: ( M -POS_prod (M --> XS) is complete & M -POS_prod (M --> XS) is continuous ) by WAYBEL20:34;
M -POS_prod (M --> (oContMaps X,Sierpinski_Space )), oContMaps X,(M -TOP_prod (M --> Sierpinski_Space )) are_isomorphic by Th36, WAYBEL_1:7;
then ( oContMaps X,MS is complete & oContMaps X,MS is continuous ) by A3, WAYBEL15:11, WAYBEL20:18;
hence ( oContMaps X,Y is complete & oContMaps X,Y is continuous ) by A2, Th24; :: thesis: verum