proposition: Lemma fun_set_to_prod8: bijection (fun_set_to_prod src F).
proof: Proof. move: (fun_set_to_prod4); set (g :=fun_set_to_prod src F). move => [fg sg tg]. split. split =>// x y; rewrite sg => xs ys. have [x0 [fx0 sx0 tx0 gx]] := (gfunctions_hi xs). have [x1 [fx1 sx1 tx1 gx1]] := (gfunctions_hi ys). have ta:=(fun_set_to_prod3). rewrite /g/fun_set_to_prod ! LfV //; clear ta; move => eq. rewrite - gx - gx1; congr graph. apply: function_exten=>//; (try ue) => x2 x2s. apply: (setXb_exten (f := F)); [ ue| rewrite sx0 - sx1 in x2s; ue |]. move=> i iF. have [[fc0 sc0 tc0] vc0] := (fun_set_to_prod1 fF iF fx0 tx0). have [[fc1 sc1 tc1] vc1] := (fun_set_to_prod1 fF iF fx1 tx1). have x0c: (x0 = triple src (productb F) x). by rewrite - sx0 -tx0 -gx corresp_recov1 //; move: fx0=>[cx0 _]. have x1c: (x1 = triple src (productb F) y). by rewrite - sx1 -tx1 -gx1 corresp_recov1 //; move: fx1=>[cx1 _]. have cc: ((pr_i F i) \co x0 = (pr_i F i) \co x1). move: (congr1 (Vg ^~i) eq). rewrite !LgV // - x0c -x1c => eq1. by apply: function_exten1 =>//; aw. by rewrite - vc0 //; rewrite sx0 - sx1 in x2s; rewrite cc - vc1. split => // y. rewrite sg {1} /g /fun_set_to_prod lf_target. move/setXf_P=> [fy]; aw; move=> dy py. set (x:= Lf (fun u=> Lg (domain F) (fun i=> Vg (Vg y i) u)) src (productb F)). have sx: source x = src by rewrite /x; aw. have tx: target x = productb F by rewrite /x; aw. have fx: function x. rewrite /x; apply: lf_function. move=> t ts; apply/setXb_P; split; aww. move => i idf; rewrite LgV //; move: (py _ idf); aw=> xpp. have [k [fk sk <- gk]] := (gfunctions_hi xpp). have ->: (Vg (Vg y i) t = Vf k t) by rewrite /Vf gk. Wtac. have gs: inc (graph x) (gfunctions src (productb F)). rewrite - sx -tx; apply: gfunctions_i=> //. ex_tac. move: (fun_set_to_prod3) => ax. rewrite /g/fun_set_to_prod; rewrite LfV //; clear ax. symmetry;apply: fgraph_exten; aw;fprops =>//. move=> z zd; rewrite LgV //;move: (py _ zd); aw; move => Vzg. have xp: (x = triple src (productb F) (graph x)). by rewrite - sx -tx corresp_recov1 //; move: fx=>[cx _]. rewrite - xp. have [x1 [fx1 sx1 tx1 gx1]] := (gfunctions_hi Vzg). suff: (x1 = (pr_i F z) \co x) by move => <-. apply: function_exten =>//; try fct_tac; try (rewrite /pr_i; aw; ue). by apply: pri_f. move =>// x0 z0s. have x0s: inc x0 src by ue. have x0s': inc x0 (source x) by ue. have cc: (pr_i F z) \coP x. split => //; [apply: pri_f=>//| rewrite /pr_i; aw; ue]. have Wp: inc (Vf x x0) (productb F) by Wtac. rewrite compfV // pri_V // /x LfV //. rewrite LgV // /Vf; ue. move=> t ts /=; apply /setXb_P; split;aww. move=> i id; aw; move: (py _ id); aw => aux. move: (gfunctions_hi aux) => [x2 [fx2 sx2 tx2 gx2]]. rewrite LgV // -tx2 -gx2 - [Vg _ _] /(Vf x2 t); Wtac. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)