proposition: Lemma prod_of_products_V f f' i: inc i (source f) -> Vf (prod_of_products f f') i = (Vf f i) \times (Vf f' i).
proof: Proof. move=> isf;rewrite LfV // => x xs; apply /funI_P; ex_tac. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)