proposition: Theorem prj_fs f J: nonempty_fam f -> sub J (domain f) -> surjection (pr_j f J).
proof: Proof. move=> alne sjd;split; first by apply: prj_f. rewrite /pr_j=> y; aw; move/setXb_P. aw;move => [fy dy iVVy]. have iVV: (forall i, inc i J -> inc (Vg y i) (Vg f i)). by move => i ij; move: (iVVy _ ij); rewrite LgV. move: (extension_psetX alne fy dy sjd iVV) => [h [dh fgh iVVh sv]]. have hp: (inc h (productb f)) by apply/setXb_P. ex_tac; rewrite prj_V //; rewrite -dh in sjd. apply: fgraph_exten; aw;fprops=> x; rewrite dy => xd. by rewrite LgV // sv. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)