let X, Y be non empty 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
P1: ( 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 ThHOM02A;
consider J being Function of [:(product X),(product Y):],(product <*(product X),(product Y)*>) such that
P2: ( 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 Element of 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 ThHOM02;
P7: rng J = the carrier of (product <*(product X),(product Y)*>) by P2, 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 FUNCT_2:31, P2;
P4: ( dom (J ") = rng J & rng (J ") = dom J ) by FUNCT_1:55, P2;
then P5: dom (J ") = the carrier of (product <*(product X),(product Y)*>) by P2, FUNCT_2:def 3;
P6: rng (J ") = the carrier of [:(product X),(product Y):] by P4, 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 P1, P2; :: thesis:
rng K = the carrier of (product (X ^ Y)) by FUNCT_2:def 3, P1;
then rng I = the carrier of (product (X ^ Y)) by FUNCT_2:20, P6;
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
H1: ( x = x1 & y = y1 & K . (x,y) = x1 ^ y1 ) by P1;
H2: J . (x,y) = <*x,y*> by P2;
[x,y] in the carrier of [:(product X),(product Y):] ;
then H4: [x,y] in dom J by FUNCT_2:def 1;
<*x,y*> is Point of (product <*(product X),(product Y)*>) by ThZ03A;
then I . <*x,y*> = K . (JB . (J . [x,y])) by H2, P5, FUNCT_1:23;
then I . <*x,y*> = x1 ^ y1 by H1, H4, FUNCT_1:56, P2;
hence ex x1, y1 being FinSequence st
( x = x1 & y = y1 & I . <*x,y*> = x1 ^ y1 ) by H1; :: 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
S1: v = J . x by P7, FUNCT_2:190;
consider y being Element of the carrier of [:(product X),(product Y):] such that
S2: w = J . y by P7, FUNCT_2:190;
( 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 S1A: ( JB . v = x & JB . w = y & JB . (J . (x + y)) = x + y ) by S1, S2, FUNCT_1:56, P2;
( v in rng J & w in rng J ) by P7;
then S1D: ( v in dom JB & w in dom JB ) by FUNCT_1:55, P2;
v + w = J . (x + y) by S1, S2, P2;
then I . (v + w) = K . (x + y) by S1A, P5, FUNCT_1:23
.= (K . x) + (K . y) by P1
.= ((K * JB) . v) + (K . (JB . w)) by S1A, S1D, FUNCT_1:23 ;
hence I . (v + w) = (I . v) + (I . w) by S1D, FUNCT_1:23; :: 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
S1: v = J . x by P7, FUNCT_2:190;
x in the carrier of [:(product X),(product Y):] ;
then x in dom J by FUNCT_2:def 1;
then S1A: JB . v = x by S1, FUNCT_1:56, P2;
v in rng J by P7;
then S1D: v in dom JB by FUNCT_1:55, P2;
r * x in the carrier of [:(product X),(product Y):] ;
then S4: r * x in dom J by FUNCT_2:def 1;
r * v = J . (r * x) by S1, P2;
then I . (r * v) = K . (JB . (J . (r * x))) by P5, FUNCT_1:23;
hence I . (r * v) = K . (r * x) by S4, FUNCT_1:56, P2
.= r * (K . x) by P1
.= r * (I . v) by S1A, S1D, FUNCT_1:23 ;
:: 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 S1B: 0. [:(product X),(product Y):] in dom J by FUNCT_2:def 1;
0. (product <*(product X),(product Y)*>) in rng J by P7;
then 0. (product <*(product X),(product Y)*>) in dom JB by FUNCT_1:55, P2;
then I . (0. (product <*(product X),(product Y)*>)) = K . (JB . (J . (0. [:(product X),(product Y):]))) by P2, FUNCT_1:23;
hence I . (0. (product <*(product X),(product Y)*>)) = 0. (product (X ^ Y)) by P1, S1B, FUNCT_1:56, P2; :: 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
S1: v = J . x by P7, FUNCT_2:190;
x in the carrier of [:(product X),(product Y):] ;
then S1B: x in dom J by FUNCT_2:def 1;
v in rng J by P7;
then v in dom JB by FUNCT_1:55, P2;
then I . v = K . (JB . (J . x)) by S1, FUNCT_1:23
.= K . x by S1B, FUNCT_1:56, P2 ;
then ||.(I . v).|| = ||.x.|| by P1;
hence ||.(I . v).|| = ||.v.|| by P2, S1; :: thesis:

end;