fact: Definition dprod_as_csb_fun: CSetoid_bin_fun (ProdCSetoid M1 M2) (ProdCSetoid M1 M2)(ProdCSetoid M1 M2):= (Build_CSetoid_bin_fun (ProdCSetoid M1 M2)(ProdCSetoid M1 M2) (ProdCSetoid M1 M2) dprod dprod_strext).
imports: CoRN.algebra.CSetoidInc