theorem :: VECTSP12:17

for K being Ring
for X, Y being VectorSpace-Sequence of K ex I being Function of [:(product X),(product Y):],(product (X ^ Y)) st
( I is one-to-one & I is onto & ( for x being Vector of (product X)
for y being Vector of (product Y) ex x1, y1 being FinSequence st
( x = x1 & y = y1 & I . (x,y) = x1 ^ y1 ) ) & ( for v, w being Vector of [:(product X),(product Y):] holds I . (v + w) = (I . v) + (I . w) ) & ( for v being Vector of [:(product X),(product Y):]
for r being Element of the carrier of K holds I . (r * v) = r * (I . v) ) & I . (0. [:(product X),(product Y):]) = 0. (product (X ^ Y)) )