proposition: Lemma fun_set_to_prod4 : function_prop (fun_set_to_prod src F) (gfunctions src (productb F)) (productb (Lg (domain F) (fun i=> gfunctions src (Vg F i)))).
proof: Proof. rewrite/fun_set_to_prod; hnf;aw; split => //. by apply: lf_function; apply: fun_set_to_prod3. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)