--- a/src/HOL/Analysis/FPS_Convergence.thy	Tue Apr 22 22:06:52 2025 +0100
+++ b/src/HOL/Analysis/FPS_Convergence.thy	Wed Apr 23 01:38:06 2025 +0200
@@ -691,6 +691,10 @@
   finally show ?thesis .
 qed
 
+lemma eval_fps_has_fps_expansion:
+  "fps_conv_radius F > 0 \<Longrightarrow> eval_fps F has_fps_expansion F"
+  unfolding has_fps_expansion_def by simp
+
 lemma has_fps_expansion_imp_continuous:
   fixes F :: "'a::{real_normed_field,banach} fps"
   assumes "f has_fps_expansion F"