proposition: Lemma big_prod_subfieldP (I : finType) (D : {pred I}) (K : fieldType) (aT : fieldExtType K) (U : I -> {vspace aT}) (W : {subfield aT}) : reflect (forall u : I -> aT, (forall i, D i -> u i \in U i) -> \prod_(i in D) u i \in W) (\big[@prodv _ _/1%VS]_(i in D) U i <= W)%VS.
proof: Proof. by apply/big_prod_subfield_seqP/index_enum_uniq. Qed.
imports: HB(structures) mathcomp(all_ssreflect all_fingroup all_algebra all_solvable) mathcomp(all_field)