:: deftheorem Defm defines vector_mult VECTSP13:def 6 :
for R being Ring
for n being Nat
for b₃ being Function of [: the carrier of R,(n -tuples_on the carrier of R):],(n -tuples_on the carrier of R) holds
( b₃ = vector_mult (n,R) iff for a being Element of R
for u being Tuple of n, the carrier of R holds b₃ . (a,u) = a * u );