theorem ConormProd: :: FUZNORM1:28

conorm prodnorm = probsum_conorm