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