proposition: Lemma prj_axiom: lf_axiom (restr^~ J) (productb f)(restriction_product f J).
proof: Proof. move=> x /setXb_P [fx dx iVV]. have sx: sub J (domain x) by rewrite dx. apply/setXb_P; aw; split; fprops. by move=> i ij; rewrite !LgV //; apply: iVV; apply: jdf. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)