theorem Th12: :: VECTSP12:16

for K being Ring
for X, Y being VectSp of K ex I being Function of [:X,Y:],(product <*X,Y*>) st
( I is one-to-one & I is onto & ( for x being Vector of X
for y being Vector of Y holds I . (x,y) = <*x,y*> ) & ( for v, w being Vector of [:X,Y:] holds I . (v + w) = (I . v) + (I . w) ) & ( for v being Vector of [:X,Y:]
for r being Element of K holds I . (r * v) = r * (I . v) ) & I . (0. [:X,Y:]) = 0. (product <*X,Y*>) )