let X be non empty TopSpace; ( 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
; 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; ( 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; verum