proposition: Lemma MVP_CR_apply_prf_2 : forall n (morph : MultivariatePolynomial CRasCRing n -> n_Function (msp_as_RSetoid CR) (msp_as_RSetoid CR) n) (morph_prf : forall x1 x2 : MultivariatePolynomial CRasCRing n, x1 [=] x2 -> morph x1 [=] morph x2) (p1 p2 : cpoly_cring (MultivariatePolynomial CRasCRing n)), p1 [=] p2 -> extEq (n_Function (msp_as_RSetoid CR) (msp_as_RSetoid CR) n) (fun x : RegularFunction Qball => morph p1 ! (MVP_C_ CRasCRing n x)) (fun x : RegularFunction Qball => morph p2 ! (MVP_C_ CRasCRing n x)).
proof: Proof. intros. intro x. simpl. apply morph_prf, cpoly_apply_wd. exact H. apply csf_wd. reflexivity. Qed.
imports: CoRN.algebra.RSetoid CoRN.metric2.Metric CoRN.metric2.UniformContinuity CoRN.algebra.Bernstein CoRN.algebra.CRing_Homomorphisms CoRN.algebra.COrdFields2 CoRN.model.ordfields.Qordfield CoRN.model.totalorder.QMinMax CoRN.tactics.CornTac CoRN.tactics.Qauto CoRN.model.metric2.Qmetric Coq.QArith.Qabs CoRN.reals.fast.CRabs CoRN.reals.fast.ModulusDerivative CoRN.reals.fast.CRArith CoRN.reals.fast.CRArith_alg CoRN.algebra.RSetoid