for n being Nat
for K being Field
for a being Element of K
for v, v1, v2 being Vector of (n -VectSp_over K)
for t, t1, t2 being Element of n -tuples_on the carrier of K holds
( the carrier of (n -VectSp_over K) = n -tuples_on the carrier of K & 0. (n -VectSp_over K) = n |-> (0. K) & ( t1 = v1 & t2 = v2 implies t1 + t2 = v1 + v2 ) & ( t = v implies a * t = a * v ) )