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