proposition: Lemma setXb_P f x: inc x (productb f) <-> [/\ fgraph x, domain x = domain f & forall i, inc i (domain f) -> inc (Vg x i) (Vg f i)].
proof: Proof. split; first by move/Zo_P => [] //. move => [pa pb pc]; apply: Zo_i => //; apply/setP_P => t tx. have gx: (sgraph x) by fprops. have aux: inc (P t) (domain f) by rewrite - pb; apply: domain_i1. rewrite - (gx _ tx); apply: setXp_i => //. by apply /setUb_P; ex_tac; rewrite (pr2_V pa tx); apply: pc. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)