theorem Th15: :: PRVECT_4:10

for X, Y, Z being RealNormSpace ex I being Function of [:X,Y,Z:],(product <*X,Y,Z*>) st
( I is one-to-one & I is onto & ( for x being Point of X
for y being Point of Y
for z being Point of Z holds I . (x,y,z) = <*x,y,z*> ) & ( for v, w being Point of [:X,Y,Z:] holds I . (v + w) = (I . v) + (I . w) ) & ( for v being Point of [:X,Y,Z:]
for r being Real holds I . (r * v) = r * (I . v) ) & 0. (product <*X,Y,Z*>) = I . (0. [:X,Y,Z:]) & ( for v being Point of [:X,Y,Z:] holds ||.(I . v).|| = ||.v.|| ) )