proposition: Lemma fun_set_to_prod3: lf_axiom(fun f => Lg (domain F)( fun i=> (graph (compose (pr_i F i) (triple src (productb F) f))))) (gfunctions src (productb F)) (productb (Lg (domain F) (fun i=> gfunctions src (Vg F i)))).
proof: Proof. move=> x xs. set (f:= triple src (productb F) x). move: (fun_set_to_prod2 xs (refl_equal f)) => [ff sf tf]. apply/setXf_P;split; aww => i id; rewrite LgV //. move: (fun_set_to_prod1 fF id ff tf) => [[fc sc tg] vc]. rewrite -/f - sf - sc -tg; apply: gfunctions_i; fprops. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)