proposition: Fact ffun_vect_iso : Vector.axiom (#|I| * dim vT) {ffun I -> vT}.
proof: Proof. pose fr (f : {ffun I -> vT}) := mxvec (\matrix_(i < #|I|) v2r (f (enum_val i))). exists fr => /= [k f g|]. rewrite /fr -linearP; congr (mxvec _); apply/matrixP=> i j. by rewrite !mxE /= !ffunE linearP !mxE. exists (fun r => [ffun i => r2v (row (enum_rank i) (vec_mx r)) : vT]) => [g|r]. by apply/ffunP=> i; rewrite ffunE mxvecK rowK v2rK enum_rankK. by apply/(canLR vec_mxK)/matrixP=> i j; rewrite mxE ffunE r2vK enum_valK mxE. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq choice) mathcomp(fintype bigop finfun tuple) mathcomp(ssralg matrix mxalgebra zmodp)