Theorem lmhmf

Description: A homomorphism of left modules is a function. (Contributed by Stefan O'Rear, 1-Jan-2015)

	Ref	Expression
Hypotheses	lmhmf.b	|- B = ( Base ` S )
	lmhmf.c	|- C = ( Base ` T )
Assertion	lmhmf	|- ( F e. ( S LMHom T ) -> F : B --> C )

Proof

Step	Hyp	Ref	Expression
1		lmhmf.b	|- B = ( Base ` S )
2		lmhmf.c	|- C = ( Base ` T )
3		lmghm	|- ( F e. ( S LMHom T ) -> F e. ( S GrpHom T ) )
4	1 2	ghmf	|- ( F e. ( S GrpHom T ) -> F : B --> C )
5	3 4	syl	|- ( F e. ( S LMHom T ) -> F : B --> C )