proposition: Lemma mxof_comp (phi : 'Hom(uT, vT)) (psi : 'Hom(vT, wT)) : mxof e g (psi \o phi)%VF = mxof e f phi *m mxof f g psi.
proof: Proof. apply/matrixP => i k; rewrite !(mxE, comp_lfunE, lfunE) /=. rewrite [phi _](coord_basis f_basis) ?memvf// 2!linear_sum/=. by apply: eq_bigr => j _ /=; rewrite !mxE !linearZ/= !vecof_delta. Qed.
imports: mathcomp(all_ssreflect all_fingroup all_algebra all_solvable)