Theorem fveere

Description: The function value of a point is a real. (Contributed by Scott Fenton, 10-Jun-2013)

	Ref	Expression
Assertion	fveere	⊢ ( ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐼 ∈ ( 1 ... 𝑁 ) ) → ( 𝐴 ‘ 𝐼 ) ∈ ℝ )

Proof

Step	Hyp	Ref	Expression
1		eleei	⊢ ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) → 𝐴 : ( 1 ... 𝑁 ) ⟶ ℝ )
2	1	ffvelrnda	⊢ ( ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐼 ∈ ( 1 ... 𝑁 ) ) → ( 𝐴 ‘ 𝐼 ) ∈ ℝ )