let X be RealLinearSpace-Sequence; :: thesis: for Y being RealLinearSpace 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*>)) )
let Y be RealLinearSpace; :: 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*>)) )
consider I being Function of [:(product X),Y:],[:(product X),(product <*Y*>):] such that
A1: ( 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*>):] ) by Th21;
consider J being Function of [:(product X),(product <*Y*>):],(product (X ^ <*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*>) 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*>)) ) by Th13;
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*>)) )
thus K is one-to-one by A1, A2; :: 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*>)) )
A3: rng J = the carrier of (product (X ^ <*Y*>)) by A2, FUNCT_2:def 3;
rng I = the carrier of [:(product X),(product <*Y*>):] by A1, FUNCT_2:def 3;
then rng (J * I) = J .: the carrier of [:(product X),(product <*Y*>):] by RELAT_1:127
.= the carrier of (product (X ^ <*Y*>)) by A3, RELSET_1:22 ;
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*>)) )
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*>)) )

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 )
A4: I . (x,y) = [x,<*y*>] by A1;
[x,y] in the carrier of [:(product X),Y:] ;
then [x,<*y*>] in the carrier of [:(product X),(product <*Y*>):] by A4, FUNCT_2:5;
then reconsider yy = <*y*> as Point of (product <*Y*>) by ZFMISC_1:87;
consider x1, y1 being FinSequence such that
A5: ( x = x1 & yy = y1 & J . (x,yy) = x1 ^ y1 ) by A2;
J . (x,yy) = J . (I . [x,y]) by A4
.= K . (x,y) by FUNCT_2:15 ;
hence ex x1, y1 being FinSequence st
( x = x1 & <*y*> = y1 & K . (x,y) = x1 ^ y1 ) by A5; :: 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*>)) )

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:15
.= J . ((I . v) + (I . w)) by A1
.= (J . (I . v)) + (J . (I . w)) by A2
.= (K . v) + (J . (I . w)) by FUNCT_2:15
.= (K . v) + (K . w) by FUNCT_2:15 ; :: 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*>))

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:15
.= J . (r * (I . v)) by A1
.= r * (J . (I . v)) by A2
.= r * (K . v) by FUNCT_2:15 ; :: thesis: verum

end;

thus K . (0. [:(product X),Y:]) = 0. (product (X ^ <*Y*>)) by A1, A2, FUNCT_2:15; :: thesis: verum