let X, Y be RealNormSpace-Sequence; :: thesis:
set PX = product X;
set PY = product Y;
set PXY = product (X ^ Y);
consider K being Function of [:(product X),(product Y):],(product (X ^ Y)) such that
A1: ( K is one-to-one & K 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 & K . (x,y) = x1 ^ y1 ) ) & ( for v, w being Point of [:(product X),(product Y):] holds K . (v + w) = (K . v) + (K . w) ) & ( for v being Point of [:(product X),(product Y):]
for r being Element of REAL holds K . (r * v) = r * (K . v) ) & K . (0. [:(product X),(product Y):]) = 0. (product (X ^ Y)) & ( for v being Point of [:(product X),(product Y):] holds ||.(K . v).|| = ||.v.|| ) ) by Th17;
consider J being Function of [:(product X),(product Y):],(product <*(product X),(product Y)*>) such that
A2: ( J is one-to-one & J is onto & ( for x being Point of (product X)
for y being Point of (product Y) holds J . (x,y) = <*x,y*> ) & ( for v, w being Point of [:(product X),(product Y):] holds J . (v + w) = (J . v) + (J . w) ) & ( for v being Point of [:(product X),(product Y):]
for r being Real holds J . (r * v) = r * (J . v) ) & 0. (product <*(product X),(product Y)*>) = J . (0. [:(product X),(product Y):]) & ( for v being Point of [:(product X),(product Y):] holds ||.(J . v).|| = ||.v.|| ) ) by Th15;
A3: rng J = the carrier of (product <*(product X),(product Y)*>) by A2, FUNCT_2:def 3;
then reconsider JB = J " as Function of the carrier of (product <*(product X),(product Y)*>), the carrier of [:(product X),(product Y):] by A2, FUNCT_2:25;
A4: ( dom (J ") = rng J & rng (J ") = dom J ) by A2, FUNCT_1:33;
then A5: dom (J ") = the carrier of (product <*(product X),(product Y)*>) by A2, FUNCT_2:def 3;
A6: rng (J ") = the carrier of [:(product X),(product Y):] by A4, FUNCT_2:def 1;
reconsider I = K * JB as Function of (product <*(product X),(product Y)*>),(product (X ^ Y)) ;
take I ; :: thesis:
thus I is one-to-one by A1, A2; :: thesis:
rng K = the carrier of (product (X ^ Y)) by A1, FUNCT_2:def 3;
then rng I = the carrier of (product (X ^ Y)) by A6, FUNCT_2:14;
hence I is onto by FUNCT_2:def 3; :: thesis:
thus 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 ) :: thesis:

proof

let x be Point of (product X); :: thesis:
let y be Point of (product Y); :: thesis:
consider x1, y1 being FinSequence such that
A7: ( x = x1 & y = y1 & K . (x,y) = x1 ^ y1 ) by A1;
A8: J . (x,y) = <*x,y*> by A2;
[x,y] in the carrier of [:(product X),(product Y):] ;
then A9: [x,y] in dom J by FUNCT_2:def 1;
I . <*x,y*> = K . (JB . (J . [x,y])) by A8, A5, FUNCT_1:13;
then I . <*x,y*> = x1 ^ y1 by A7, A9, A2, FUNCT_1:34;
hence ex x1, y1 being FinSequence st
( x = x1 & y = y1 & I . <*x,y*> = x1 ^ y1 ) by A7; :: thesis:

end;

thus for v, w being Point of (product <*(product X),(product Y)*>) holds I . (v + w) = (I . v) + (I . w) :: thesis:

proof

let v, w be Point of (product <*(product X),(product Y)*>); :: thesis:
consider x being Element of the carrier of [:(product X),(product Y):] such that
A10: v = J . x by A3, FUNCT_2:113;
consider y being Element of the carrier of [:(product X),(product Y):] such that
A11: w = J . y by A3, FUNCT_2:113;
( x in the carrier of [:(product X),(product Y):] & y in the carrier of [:(product X),(product Y):] & x + y in the carrier of [:(product X),(product Y):] ) ;
then ( x in dom J & y in dom J & x + y in dom J ) by FUNCT_2:def 1;
then A12: ( JB . v = x & JB . w = y & JB . (J . (x + y)) = x + y ) by A10, A11, A2, FUNCT_1:34;
( v in rng J & w in rng J ) by A3;
then A13: ( v in dom JB & w in dom JB ) by A2, FUNCT_1:33;
v + w = J . (x + y) by A10, A11, A2;
then I . (v + w) = K . (x + y) by A12, A5, FUNCT_1:13
.= (K . x) + (K . y) by A1
.= ((K * JB) . v) + (K . (JB . w)) by A12, A13, FUNCT_1:13 ;
hence I . (v + w) = (I . v) + (I . w) by A13, FUNCT_1:13; :: thesis:

end;

thus for v being Point of (product <*(product X),(product Y)*>)
for r being Element of REAL holds I . (r * v) = r * (I . v) :: thesis:

proof

let v be Point of (product <*(product X),(product Y)*>); :: thesis:
let r be Element of REAL ; :: thesis:
consider x being Element of the carrier of [:(product X),(product Y):] such that
A14: v = J . x by A3, FUNCT_2:113;
x in the carrier of [:(product X),(product Y):] ;
then x in dom J by FUNCT_2:def 1;
then A15: JB . v = x by A14, A2, FUNCT_1:34;
v in rng J by A3;
then A16: v in dom JB by A2, FUNCT_1:33;
r * x in the carrier of [:(product X),(product Y):] ;
then A17: r * x in dom J by FUNCT_2:def 1;
r * v = J . (r * x) by A14, A2;
then I . (r * v) = K . (JB . (J . (r * x))) by A5, FUNCT_1:13;
hence I . (r * v) = K . (r * x) by A17, A2, FUNCT_1:34
.= r * (K . x) by A1
.= r * (I . v) by A15, A16, FUNCT_1:13 ;
:: thesis:

end;

thus I . (0. (product <*(product X),(product Y)*>)) = 0. (product (X ^ Y)) :: thesis:

proof

0. [:(product X),(product Y):] in the carrier of [:(product X),(product Y):] ;
then A18: 0. [:(product X),(product Y):] in dom J by FUNCT_2:def 1;
0. (product <*(product X),(product Y)*>) in rng J by A3;
then 0. (product <*(product X),(product Y)*>) in dom JB by A2, FUNCT_1:33;
then I . (0. (product <*(product X),(product Y)*>)) = K . (JB . (J . (0. [:(product X),(product Y):]))) by A2, FUNCT_1:13;
hence I . (0. (product <*(product X),(product Y)*>)) = 0. (product (X ^ Y)) by A1, A18, A2, FUNCT_1:34; :: thesis:

end;

thus for v being Point of (product <*(product X),(product Y)*>) holds ||.(I . v).|| = ||.v.|| :: thesis:

proof

let v be Point of (product <*(product X),(product Y)*>); :: thesis:
consider x being Element of the carrier of [:(product X),(product Y):] such that
A19: v = J . x by A3, FUNCT_2:113;
x in the carrier of [:(product X),(product Y):] ;
then A20: x in dom J by FUNCT_2:def 1;
v in rng J by A3;
then v in dom JB by A2, FUNCT_1:33;
then I . v = K . (JB . (J . x)) by A19, FUNCT_1:13
.= K . x by A20, A2, FUNCT_1:34 ;
then ||.(I . v).|| = ||.x.|| by A1;
hence ||.(I . v).|| = ||.v.|| by A2, A19; :: thesis:

end;