proposition: Lemma prod_of_function_axioms x x': inc (graph x) (productb (graph f)) -> inc (graph x') (productb (graph f')) -> lf_axiom (fun i => J (Vf x i) (Vf x' i)) (source f) (union (prod_of_prod_target f f')).
proof: Proof. move=> gp gp' y ys. apply: (@setU_i _ ((Vf f y) \times (Vf f' y))); last by apply/funI_P; ex_tac. apply/setXp_i. move /setXb_P: gp=> [fgx dgx p1]; apply:p1; rewrite domain_fg //. move /setXb_P: gp'=> [fgx dgx p1]; apply:p1; rewrite domain_fg //; ue. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)