for m being Element of M holds (M => S) . m is injective ;
hence M -TOP_prod (M => S) is injective by WAYBEL18:7; :: thesis: verum