Multiplication of a vector-quantity by a scalar-quantity results in a vector-quantity. The product is equal to the vector-quantity constructed by multiplying each component of the argument vector by the argument scalar.The * function is commutative for scalar/vector pairs.
(=> (And (Vector-Quantity ?V1) (Scalar-Quantity ?S)) (= (* ?V1 ?S) (* ?S ?V1))) (=> (And (Scalar-Quantity ?S) (Vector-Quantity ?V1) (* ?S ?V1 ?V)) (And (Vector-Quantity ?V) (= (Spatial.Dimension ?V1) (Spatial.Dimension ?V)) (Forall (?B ?I) (=> (= (Basis.Dimension ?B) (Spatial.Dimension ?V1)) (= (Vector-Component ?V ?I ?B) (* ?S (Vector-Component ?V1 ?I ?B)))))))