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