Theorem fveere

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

	Ref	Expression
Assertion	fveere	$$⊢\left(A\in 𝔼\left(N\right)\wedge I\in \left(1\dots N\right)\right)\to A\left(I\right)\in ℝ$$

Proof

Step	Hyp	Ref	Expression
1		eleei	$$⊢A\in 𝔼\left(N\right)\to A:\left(1\dots N\right)⟶ℝ$$
2	1	ffvelrnda	$$⊢\left(A\in 𝔼\left(N\right)\wedge I\in \left(1\dots N\right)\right)\to A\left(I\right)\in ℝ$$