proposition: Lemma bigcat_basis Us (U := (\sum_(i | P i) Us i)%VS) : directv U -> (forall i, P i -> basis_of (Us i) (Xs i)) -> basis_of U (\big[cat/[::]]_(i | P i) Xs i).
proof: Proof. move=> dxU XsUs; rewrite /basis_of span_bigcat. have defUs i: P i -> span (Xs i) = Us i by case/XsUs/andP=> /eqP. rewrite (eq_bigr _ defUs) eqxx bigcat_free // => [|_ /XsUs/andP[]//]. apply/directvP; rewrite /= (eq_bigr _ defUs) (directvP dxU) /=. by apply/eq_bigr=> i /defUs->. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq choice) mathcomp(fintype bigop finfun tuple) mathcomp(ssralg matrix mxalgebra zmodp)