proposition: Lemma span_lfunP (U : seq uT) (phi psi : 'Hom(uT,vT)) : {in <<U>>%VS, phi =1 psi} <-> {in U, phi =1 psi}.
proof: Proof. split=> eq_phi_psi u uU; first by rewrite eq_phi_psi ?memv_span. rewrite [u](@coord_span _ _ _ (in_tuple U))// !linear_sum/=. by apply: eq_bigr=> i _; rewrite !linearZ/= eq_phi_psi// ?mem_nth. Qed.
imports: mathcomp(all_ssreflect all_fingroup all_algebra all_solvable)