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 )
consider M being non empty set , f being Function of T,(product (M --> Sierpinski_Space )) such that
A2: corestr f is being_homeomorphism by Th19;
thus ex M being non empty set st T is_Retract_of product (M --> Sierpinski_Space ) by A1, A2, Th12; :: thesis: verum