Definition setwith2binopdirprod (X Y : setwith2binop) : setwith2binop. Proof. exists (setdirprod X Y). simpl. exact ( (λ xy xy', (op1 (pr1 xy) (pr1 xy')) ,, (op1 (pr2 xy) (pr2 xy'))) ,, (λ xy xy', (op2 (pr1 xy) (pr1 xy')) ,, (op2 (pr2 xy) (pr2 xy'))) ). Defined.