let T be T_0-TopSpace; :: thesis: ( T is injective implies ex M being non empty set st T is_Retract_of product (M --> Sierpinski_Space ) )
assume A1: T is injective ; :: thesis: ex M being non empty set st T is_Retract_of product (M --> Sierpinski_Space )
ex M being non empty set ex f being Function of T,(product (M --> Sierpinski_Space )) st corestr f is being_homeomorphism by Th19;
hence ex M being non empty set st T is_Retract_of product (M --> Sierpinski_Space ) by A1, Th12; :: thesis: verum