proposition: Lemma big_prod_subfield_seqP (I : eqType) (r : seq I) (r_uniq : uniq r) (P : {pred I}) (K : fieldType) (aT : fieldExtType K) (U : I -> {vspace aT}) (W : {subfield aT}) : reflect (forall u : I -> aT, (forall i, P i -> u i \in U i) -> \prod_(i <- r | P i) u i \in W) (\big[@prodv _ _/1%VS]_(i <- r | P i) U i <= W)%VS.
proof: Proof. apply: (iffP (big_prodv_seqP _ _ _ _ _)) => // [WP u uU|WP u v uU vV]. by apply: WP; rewrite ?mem1v. by rewrite -big_change_idx/= memvM ?WP//; apply/subvP: uU; rewrite sub1v. Qed.
imports: HB(structures) mathcomp(all_ssreflect all_fingroup all_algebra all_solvable) mathcomp(all_field)