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