theorem Th23: :: PRVECT_3:23

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