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