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 Th18;
hence ex M being non empty set st T is_Retract_of product (M --> Sierpinski_Space) by A1, Th11; :: thesis: verum