[STATEMENT]
lemma NSLIM_Re: "f \<midarrow>a\<rightarrow>\<^sub>N\<^sub>S L \<Longrightarrow> (\<lambda>x. Re (f x)) \<midarrow>a\<rightarrow>\<^sub>N\<^sub>S Re L"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. f \<midarrow>a\<rightarrow>\<^sub>N\<^sub>S L \<Longrightarrow> (\<lambda>x. Re (f x)) \<midarrow>a\<rightarrow>\<^sub>N\<^sub>S Re L
[PROOF STEP]
by (simp add: NSLIM_def starfunC_approx_Re_Im_iff hRe_hcomplex_of_complex)