Theorem grpplusf

Description: The group addition operation is a function. (Contributed by Mario Carneiro, 14-Aug-2015)

	Ref	Expression
Hypotheses	grpplusf.1	|- B = ( Base ` G )
	grpplusf.2	|- F = ( +f ` G )
Assertion	grpplusf	|- ( G e. Grp -> F : ( B X. B ) --> B )

Proof

Step	Hyp	Ref	Expression
1		grpplusf.1	|- B = ( Base ` G )
2		grpplusf.2	|- F = ( +f ` G )
3		grpmnd	|- ( G e. Grp -> G e. Mnd )
4	1 2	mndplusf	|- ( G e. Mnd -> F : ( B X. B ) --> B )
5	3 4	syl	|- ( G e. Grp -> F : ( B X. B ) --> B )