Theorem rrxf

Description: Euclidean vectors as functions. (Contributed by Thierry Arnoux, 7-Jul-2019)

	Ref	Expression
Hypotheses	rrxmval.1	|- X = { h e. ( RR ^m I ) | h finSupp 0 }
	rrxf.1	|- ( ph -> F e. X )
Assertion	rrxf	|- ( ph -> F : I --> RR )

Proof

Step	Hyp	Ref	Expression
1		rrxmval.1	|- X = { h e. ( RR ^m I ) | h finSupp 0 }
2		rrxf.1	|- ( ph -> F e. X )
3	1	ssrab3	|- X C_ ( RR ^m I )
4	3 2	sseldi	|- ( ph -> F e. ( RR ^m I ) )
5		elmapi	|- ( F e. ( RR ^m I ) -> F : I --> RR )
6	4 5	syl	|- ( ph -> F : I --> RR )