S . m,m9 = S . [m,m9] ;
hence S . m,m9 is Morphism of D ; :: thesis: verum