Theorem vrmdf

Description: The mapping from the index set to the generators is a function into the free monoid. (Contributed by Mario Carneiro, 27-Feb-2016)

	Ref	Expression
Hypothesis	vrmdfval.u	|- U = ( varFMnd ` I )
Assertion	vrmdf	|- ( I e. V -> U : I --> Word I )

Proof

Step	Hyp	Ref	Expression
1		vrmdfval.u	|- U = ( varFMnd ` I )
2	1	vrmdfval	|- ( I e. V -> U = ( j e. I |-> <" j "> ) )
3		s1cl	|- ( j e. I -> <" j "> e. Word I )
4	3	adantl	|- ( ( I e. V /\ j e. I ) -> <" j "> e. Word I )
5	2 4	fmpt3d	|- ( I e. V -> U : I --> Word I )