proposition: Lemma pc_axiom: lf_axiom (fun x => x \cg (graph u)) (productb f) (productf (source u) (fun k => Vg f (Vf u k))).
proof: Proof. move=> x xp; move: (pc_axiom0 xp) => [fg cg VV]. have fu: function u by fct_tac. rewrite cg;apply/setXb_P; split. + fprops. + by rewrite domain_fg; aw. + aw => i isu. rewrite LgV // (VV _ isu) -/(Vf u i). by move /setXb_P: xp => /proj33; apply; Wtac. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)