Definition df-sm

Description: Define scalar multiplication on a normed complex vector space. (Contributed by NM, 24-Apr-2007) (New usage is discouraged.)

	Ref	Expression
Assertion	df-sm	⊢ ·𝑠OLD = ( 2nd ∘ 1st )

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		cns	⊢ ·𝑠OLD
1		c2nd	⊢ 2nd
2		c1st	⊢ 1st
3	1 2	ccom	⊢ ( 2nd ∘ 1st )
4	0 3	wceq	⊢ ·𝑠OLD = ( 2nd ∘ 1st )