Axiom ax-hfvadd

Description: Vector addition is an operation on ~H . (Contributed by NM, 16-Aug-1999) (New usage is discouraged.)

	Ref	Expression
Assertion	ax-hfvadd	⊢ +ℎ : ( ℋ × ℋ ) ⟶ ℋ

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		cva	⊢ +ℎ
1		chba	⊢ ℋ
2	1 1	cxp	⊢ ( ℋ × ℋ )
3	2 1 0	wf	⊢ +ℎ : ( ℋ × ℋ ) ⟶ ℋ