proposition: Lemma kHomExtendP : kHom K <<E; x>> kHomExtend.
proof: Proof. have [fM idKf] := kHomP homKf. apply/kHomP; split=> [|z Kz]; last by rewrite kHomExtend_id ?(subvP sKE) ?idKf. move=> _ _ /Fadjoin_polyP[p Ep ->] /Fadjoin_polyP[q Eq ->]. rewrite -hornerM !kHomExtend_poly ?rpredM // -hornerM; congr _.[_]. apply/polyP=> i; rewrite coef_map !coefM /= linear_sum /=. by apply: eq_bigr => j _; rewrite !coef_map /= fM ?(polyOverP _). Qed.
imports: HB(structures) mathcomp(ssreflect ssrbool ssrfun eqtype ssrnat seq div) mathcomp(choice fintype tuple finfun bigop ssralg poly) mathcomp(polydiv finset fingroup morphism quotient perm) mathcomp(action zmodp cyclic matrix mxalgebra vector) mathcomp(falgebra fieldext separable)