proposition: Theorem pam_fb f g: prod_assoc_axioms f g -> bijection (prod_assoc_map f g).
proof: Proof. move=> pa; split; first by apply: pam_fi. split; first by apply: pam_f. have sp: source (prod_assoc_map f g) = productb f by rewrite /prod_assoc_map; aw. have tp: target (prod_assoc_map f g) = (productf (domain g) (fun l => restriction_product f (Vg g l))). by rewrite /prod_assoc_map; aw. rewrite sp tp; move=> y yp; move /setXf_P: (yp); aw; move => [fy dy iVr]. move: (pa) => [fg md ugdf]. have sVd: forall i, inc i (domain g) -> sub (Vg g i) (domain f). by move=> i id v vV; rewrite -ugdf; union_tac. pose h i := Lf (fun z => (Vg (Vg y i) z)) (Vg g i) (unionb f). have ta:forall i, inc i (domain g) -> lf_axiom (fun z => Vg (Vg y i) z) (Vg g i) (unionb f). move=> i id x xV; move: (sVd _ id) =>sVdi. apply: (@setUb_i _ x); first by apply: sVdi=>//. move: (iVr _ id); aw; move/setXb_P => [fgV deq]; aw => rel. by move: (rel _ xV); rewrite !LgV. have afp: forall i, inc i (domain g) -> function_prop (h i) (Vg g i) (unionb f). move=> i id; rewrite /h. by split; first (by apply: lf_function; apply: ta); aw. move: (extension_partition_thm pa afp) => [x [[[fx sx tx] ag] etc]]. have gxp: inc (graph x) (productb f). apply/setXb_P; rewrite (domain_fg fx) - sx;split; fprops. move=> i ix; rewrite -/(Vf x i). move: ix; rewrite sx -ugdf; move/(setUb_P) =>[z zdg iV]. move: (ag _ zdg)=> [_ _ eq]; rewrite (eq _ iV) LfV //. move: (iVr _ zdg); aw; move/setXb_P => [qa]; aw => eq1 res. by move: (res _ iV); rewrite !LgV. by apply: (ta _ zdg). have Wt: inc (Vf (prod_assoc_map f g)(graph x))(target (prod_assoc_map f g)). by Wtac; apply: pam_f. ex_tac; apply: (setXf_exten (x:=y) (x':= Vf _ _ ) yp). by rewrite - tp. move=> i id. have aux2: sub (Vg g i) (domain f) by apply: sVd. have aux3: sub (Vg g i) (domain (graph x)) by rewrite domain_fg //; ue. rewrite pam_V // LgV // prj_V //. move: (iVr _ id); aw; move/setXb_P=> [fgy]; aw => qa qb. apply: fgraph_exten; aw; fprops. move: (ag _ id)=> [aa bb cc]. move => j; rewrite qa => jd; move: (cc _ jd); rewrite LgV //. by rewrite -/(Vf x j) => ->; rewrite LfV //; apply: ta. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)