proposition: Lemma aimg_cap (K : fieldType) (aT rT : fieldExtType K) (f : 'AHom(aT, rT)) (U V : {vspace aT}) : (f @: (U :&: V) = f @: U :&: f @: V)%VS.
proof: Proof. exact/lker0_img_cap/AHom_lker0. Qed.
imports: HB(structures) mathcomp(all_ssreflect all_fingroup all_algebra all_solvable) mathcomp(all_field)