let X be non empty RealNormSpace-Sequence; :: thesis: 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.|| ) )
let Y be RealNormSpace; :: thesis: 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.|| ) )
consider I being Function of [:(product X),Y:],[:(product X),(product <*Y*>):] such that
P1: ( I is one-to-one & I is onto & ( for x being Point of (product X)
for y being Point of Y holds I . (x,y) = [x,<*y*>] ) & ( 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),(product <*Y*>):] & ( for v being Point of [:(product X),Y:] holds ||.(I . v).|| = ||.v.|| ) ) by LMHOM02A1;
consider J being Function of [:(product X),(product <*Y*>):],(product (X ^ <*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*>) ex x1, y1 being FinSequence st
( x = x1 & y = y1 & J . (x,y) = x1 ^ y1 ) ) & ( 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) ) & J . (0. [:(product X),(product <*Y*>):]) = 0. (product (X ^ <*Y*>)) & ( for v being Point of [:(product X),(product <*Y*>):] holds ||.(J . v).|| = ||.v.|| ) ) by ThHOM02A;
set K = J * I;
reconsider K = J * I as Function of [:(product X),Y:],(product (X ^ <*Y*>)) ;
take K ; :: thesis: ( K is one-to-one & K 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 & K . (x,y) = x1 ^ y1 ) ) & ( for v, w being Point of [:(product X),Y:] holds K . (v + w) = (K . v) + (K . w) ) & ( for v being Point of [:(product X),Y:]
for r being Element of REAL holds K . (r * v) = r * (K . v) ) & K . (0. [:(product X),Y:]) = 0. (product (X ^ <*Y*>)) & ( for v being Point of [:(product X),Y:] holds ||.(K . v).|| = ||.v.|| ) )
thus K is one-to-one by P1, P2; :: thesis: ( K 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 & K . (x,y) = x1 ^ y1 ) ) & ( for v, w being Point of [:(product X),Y:] holds K . (v + w) = (K . v) + (K . w) ) & ( for v being Point of [:(product X),Y:]
for r being Element of REAL holds K . (r * v) = r * (K . v) ) & K . (0. [:(product X),Y:]) = 0. (product (X ^ <*Y*>)) & ( for v being Point of [:(product X),Y:] holds ||.(K . v).|| = ||.v.|| ) )
A1: rng J = the carrier of (product (X ^ <*Y*>)) by P2, FUNCT_2:def 3;
rng I = the carrier of [:(product X),(product <*Y*>):] by P1, FUNCT_2:def 3;
then rng (J * I) = J .: the carrier of [:(product X),(product <*Y*>):] by RELAT_1:160
.= the carrier of (product (X ^ <*Y*>)) by A1, RELSET_1:38 ;
hence K is onto by FUNCT_2:def 3; :: thesis: ( ( for x being Point of (product X)
for y being Point of Y ex x1, y1 being FinSequence st
( x = x1 & <*y*> = y1 & K . (x,y) = x1 ^ y1 ) ) & ( for v, w being Point of [:(product X),Y:] holds K . (v + w) = (K . v) + (K . w) ) & ( for v being Point of [:(product X),Y:]
for r being Element of REAL holds K . (r * v) = r * (K . v) ) & K . (0. [:(product X),Y:]) = 0. (product (X ^ <*Y*>)) & ( for v being Point of [:(product X),Y:] holds ||.(K . v).|| = ||.v.|| ) )
thus for x being Point of (product X)
for y being Point of Y ex x1, y1 being FinSequence st
( x = x1 & <*y*> = y1 & K . (x,y) = x1 ^ y1 ) :: thesis: ( ( for v, w being Point of [:(product X),Y:] holds K . (v + w) = (K . v) + (K . w) ) & ( for v being Point of [:(product X),Y:]
for r being Element of REAL holds K . (r * v) = r * (K . v) ) & K . (0. [:(product X),Y:]) = 0. (product (X ^ <*Y*>)) & ( for v being Point of [:(product X),Y:] holds ||.(K . v).|| = ||.v.|| ) )

proof

let x be Point of (product X); :: thesis: for y being Point of Y ex x1, y1 being FinSequence st
( x = x1 & <*y*> = y1 & K . (x,y) = x1 ^ y1 )
let y be Point of Y; :: thesis: ex x1, y1 being FinSequence st
( x = x1 & <*y*> = y1 & K . (x,y) = x1 ^ y1 )
Q1: I . (x,y) = [x,<*y*>] by P1;
[x,y] in the carrier of [:(product X),Y:] ;
then [x,<*y*>] in the carrier of [:(product X),(product <*Y*>):] by Q1, FUNCT_2:7;
then reconsider yy = <*y*> as Point of (product <*Y*>) by ZFMISC_1:106;
consider x1, y1 being FinSequence such that
Q2: ( x = x1 & yy = y1 & J . (x,yy) = x1 ^ y1 ) by P2;
J . (x,yy) = J . (I . [x,y]) by Q1
.= K . (x,y) by FUNCT_2:21 ;
hence ex x1, y1 being FinSequence st
( x = x1 & <*y*> = y1 & K . (x,y) = x1 ^ y1 ) by Q2; :: thesis: verum

end;

thus for v, w being Point of [:(product X),Y:] holds K . (v + w) = (K . v) + (K . w) :: thesis: ( ( for v being Point of [:(product X),Y:]
for r being Element of REAL holds K . (r * v) = r * (K . v) ) & K . (0. [:(product X),Y:]) = 0. (product (X ^ <*Y*>)) & ( for v being Point of [:(product X),Y:] holds ||.(K . v).|| = ||.v.|| ) )

proof

let v, w be Point of [:(product X),Y:]; :: thesis: K . (v + w) = (K . v) + (K . w)
thus K . (v + w) = J . (I . (v + w)) by FUNCT_2:21
.= J . ((I . v) + (I . w)) by P1
.= (J . (I . v)) + (J . (I . w)) by P2
.= (K . v) + (J . (I . w)) by FUNCT_2:21
.= (K . v) + (K . w) by FUNCT_2:21 ; :: thesis: verum

end;

thus for v being Point of [:(product X),Y:]
for r being Element of REAL holds K . (r * v) = r * (K . v) :: thesis: ( K . (0. [:(product X),Y:]) = 0. (product (X ^ <*Y*>)) & ( for v being Point of [:(product X),Y:] holds ||.(K . v).|| = ||.v.|| ) )

proof

let v be Point of [:(product X),Y:]; :: thesis: for r being Element of REAL holds K . (r * v) = r * (K . v)
let r be Element of REAL ; :: thesis: K . (r * v) = r * (K . v)
thus K . (r * v) = J . (I . (r * v)) by FUNCT_2:21
.= J . (r * (I . v)) by P1
.= r * (J . (I . v)) by P2
.= r * (K . v) by FUNCT_2:21 ; :: thesis: verum

end;

thus K . (0. [:(product X),Y:]) = 0. (product (X ^ <*Y*>)) by P1, P2, FUNCT_2:21; :: thesis: for v being Point of [:(product X),Y:] holds ||.(K . v).|| = ||.v.||
thus for v being Point of [:(product X),Y:] holds ||.(K . v).|| = ||.v.|| :: thesis: verum

proof

let v be Point of [:(product X),Y:]; :: thesis: ||.(K . v).|| = ||.v.||
thus ||.(K . v).|| = ||.(J . (I . v)).|| by FUNCT_2:21
.= ||.(I . v).|| by P2
.= ||.v.|| by P1 ; :: thesis: verum

end;