proposition: Lemma pri_fs f k: nonempty_fam f -> inc k (domain f) -> surjection (pr_i f k).
proof: Proof. move=> alne kd. set (J:= singleton k). have sjd: sub J (domain f) by move=> t; move/set1_P => ->. have cpc: (product1_canon (Vg f k) k) \coP (pr_i f k). split; first by apply: setX1_canon_f. by apply: pri_f. by rewrite /product1_canon /pr_i; aw. have fcpx:(function ((product1_canon (Vg f k) k) \co (pr_i f k))) by fct_tac. have prjc: (pr_j f J = (product1_canon (Vg f k) k) \co (pr_i f k)). apply: function_exten => //. - by apply: prj_f. - by rewrite /pr_j/pr_i; aw. - rewrite /pr_j/pr_i/product1_canon/product1; aw. - rewrite/restriction_product. have -> //: (restr f J) = cst_graph (singleton k) (Vg f k). by apply: Lg_exten => t /set1_P ->. - move=> x xs. have xp: inc x (productb f) by move: xs;rewrite /pr_j lf_source. have xsk: inc x (source (pr_i f k)) by rewrite /pr_i lf_source. have aux1: inc (Vf (pr_i f k) x) (Vg f k). have : (target (pr_i f k) = Vg f k) by rewrite/pr_i; aw. by move=> <-; Wtac; apply: pri_f. rewrite compfV // setX1_canon_V // prj_V //. have xp1: inc x (productb f) by []. move /setXb_P: xp1 => [fx dx iVVx]. have ssk: sub (singleton k) (domain x). by move=> xw eq1; aw; rewrite (set1_eq eq1) dx. rewrite/J; apply: fgraph_exten; rewrite /cst_graph;aww. move=> z zk; rewrite !LgV // (set1_eq zk) pri_V //. apply: (left_compose_fs2 cpc). by rewrite - prjc; apply: prj_fs. move: (setX1_canon_fb (Vg f k) k)=> [ h _]; apply: h. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)