let X, Y be non empty RealLinearSpace-Sequence; :: thesis:
reconsider CX = carr X, CY = carr Y as non empty non-empty FinSequence ;
A1: ( len CX = len X & len CY = len Y & len (carr (X ^ Y)) = len (X ^ Y) ) by PRVECT_2:def 4;
consider I being Function of [:(product CX),(product CY):],(product (CX ^ CY)) such that
P1: ( I is one-to-one & I is onto & ( for x, y being FinSequence st x in product CX & y in product CY holds
I . (x,y) = x ^ y ) ) by Th002A1;
set PX = product X;
set PY = product Y;
( len (carr (X ^ Y)) = (len X) + (len Y) & len (CX ^ CY) = (len X) + (len Y) ) by A1, FINSEQ_1:35;
then Q3: dom (carr (X ^ Y)) = dom (CX ^ CY) by FINSEQ_3:31;
Q4: for k being Nat st k in dom (carr (X ^ Y)) holds
(carr (X ^ Y)) . k = (CX ^ CY) . k

proof

let k be Nat; :: thesis:
assume R1: k in dom (carr (X ^ Y)) ; :: thesis:
then reconsider k1 = k as Element of dom (X ^ Y) by A1, FINSEQ_3:31;
A9: (carr (X ^ Y)) . k = the carrier of ((X ^ Y) . k1) by PRVECT_2:def 4;
R2: k in dom (X ^ Y) by A1, R1, FINSEQ_3:31;

per cases by R2, FINSEQ_1:38;

suppose A80: k in dom X ; :: thesis:

then A81: k in dom CX by A1, FINSEQ_3:31;
reconsider k2 = k1 as Element of dom X by A80;
thus (carr (X ^ Y)) . k = the carrier of (X . k2) by A9, FINSEQ_1:def 7
.= CX . k by PRVECT_2:def 4
.= (CX ^ CY) . k by A81, FINSEQ_1:def 7 ; :: thesis:

end;

suppose ex n being Nat st
( n in dom Y & k = (len X) + n ) ; :: thesis:

then consider n being Nat such that
A90: ( n in dom Y & k = (len X) + n ) ;
A91: n in dom CY by A1, A90, FINSEQ_3:31;
reconsider n1 = n as Element of dom Y by A90;
thus (carr (X ^ Y)) . k = the carrier of (Y . n1) by A9, A90, FINSEQ_1:def 7
.= CY . n by PRVECT_2:def 4
.= (CX ^ CY) . k by A91, A90, A1, FINSEQ_1:def 7 ; :: thesis:

end;

then Q5: carr (X ^ Y) = CX ^ CY by Q3, FINSEQ_1:17;
reconsider I = I as Function of [:(product X),(product Y):],(product (X ^ Y)) by Q3, Q4, FINSEQ_1:17;
P2: 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 )

proof

let x be Point of (product X); :: thesis:
let y be Point of (product Y); :: thesis:
reconsider x1 = x, y1 = y as FinSequence by LMPROD1;
I . (x,y) = x1 ^ y1 by P1;
hence ex x1, y1 being FinSequence st
( x = x1 & y = y1 & I . (x,y) = x1 ^ y1 ) ; :: thesis:

end;

P5: for v, w being Point of [:(product X),(product Y):] holds I . (v + w) = (I . v) + (I . w)

proof

let v, w be Point of [:(product X),(product Y):]; :: thesis:
consider x1 being Point of (product X), y1 being Point of (product Y) such that
P52: v = [x1,y1] by LM01;
consider x2 being Point of (product X), y2 being Point of (product Y) such that
P53: w = [x2,y2] by LM01;
reconsider xx1 = x1, xx2 = x2 as FinSequence by LMPROD1;
reconsider yy1 = y1, yy2 = y2 as FinSequence by LMPROD1;
reconsider xx12 = x1 + x2, yy12 = y1 + y2 as FinSequence by LMPROD1;
P4: ( dom xx1 = dom CX & dom xx2 = dom CX & dom xx12 = dom CX & dom yy1 = dom CY & dom yy2 = dom CY & dom yy12 = dom CY ) by CARD_3:18;
( I . v = I . (x1,y1) & I . w = I . (x2,y2) ) by P52, P53;
then P55: ( I . v = xx1 ^ yy1 & I . w = xx2 ^ yy2 ) by P1;
I . (v + w) = I . ((x1 + x2),(y1 + y2)) by P52, P53, defADD;
then P57: I . (v + w) = xx12 ^ yy12 by P1;
then X5: dom (xx12 ^ yy12) = dom (carr (X ^ Y)) by CARD_3:18;
reconsider Iv = I . v, Iw = I . w as Element of product (carr (X ^ Y)) ;
reconsider Ivw = (I . v) + (I . w) as FinSequence by LMPROD1;
XX1: dom Ivw = dom (carr (X ^ Y)) by CARD_3:18;
for j0 being Nat st j0 in dom Ivw holds
Ivw . j0 = (xx12 ^ yy12) . j0

proof

let j0 be Nat; :: thesis:
assume j0 in dom Ivw ; :: thesis:
then reconsider j = j0 as Element of dom (carr (X ^ Y)) by CARD_3:18;
X21: Ivw . j0 = ((addop (X ^ Y)) . j) . ((Iv . j),(Iw . j)) by PRVECT_1:def 10
.= the addF of ((X ^ Y) . j) . ((Iv . j),(Iw . j)) by PRVECT_2:def 5 ;

per cases by X21, Q3, FINSEQ_1:38;

suppose C1: j0 in dom CX ; :: thesis:

then j0 in dom X by A1, FINSEQ_3:31;
then C13: (X ^ Y) . j = X . j0 by FINSEQ_1:def 7;
C17: ( Iv . j = xx1 . j & Iw . j = xx2 . j ) by C1, P4, P55, FINSEQ_1:def 7;
F16: (xx12 ^ yy12) . j0 = xx12 . j0 by C1, P4, FINSEQ_1:def 7;
reconsider j1 = j0 as Element of dom (carr X) by C1;
the addF of ((X ^ Y) . j) . ((Iv . j),(Iw . j)) = ((addop X) . j1) . ((xx1 . j1),(xx2 . j1)) by C13, C17, PRVECT_2:def 5
.= (xx12 ^ yy12) . j0 by F16, PRVECT_1:def 10 ;
hence Ivw . j0 = (xx12 ^ yy12) . j0 by X21; :: thesis:

end;

suppose ex n being Nat st
( n in dom CY & j0 = (len CX) + n ) ; :: thesis:

then consider n being Nat such that
C1: ( n in dom CY & j0 = (len CX) + n ) ;
G2: ( len CX = len xx1 & len CX = len xx2 & len CX = len xx12 ) by P4, FINSEQ_3:31;
n in dom Y by A1, C1, FINSEQ_3:31;
then C13: (X ^ Y) . j = Y . n by C1, A1, FINSEQ_1:def 7;
C17: ( Iv . j = yy1 . n & Iw . j = yy2 . n ) by P4, P55, C1, G2, FINSEQ_1:def 7;
F16: (xx12 ^ yy12) . j0 = yy12 . n by C1, G2, P4, FINSEQ_1:def 7;
reconsider j1 = n as Element of dom (carr Y) by C1;
the addF of ((X ^ Y) . j) . ((Iv . j),(Iw . j)) = ((addop Y) . j1) . ((yy1 . j1),(yy2 . j1)) by C13, C17, PRVECT_2:def 5
.= (xx12 ^ yy12) . j0 by F16, PRVECT_1:def 10 ;
hence Ivw . j0 = (xx12 ^ yy12) . j0 by X21; :: thesis:

end;

hence I . (v + w) = (I . v) + (I . w) by P57, X5, XX1, FINSEQ_1:17; :: thesis:

end;

P6: for v being Point of [:(product X),(product Y):]
for r being Element of REAL holds I . (r * v) = r * (I . v)

proof

let v be Point of [:(product X),(product Y):]; :: thesis:
let r be Element of REAL ; :: thesis:
consider x1 being Point of (product X), y1 being Point of (product Y) such that
P52: v = [x1,y1] by LM01;
reconsider xx1 = x1, yy1 = y1 as FinSequence by LMPROD1;
reconsider rxx1 = r * x1, ryy1 = r * y1 as FinSequence by LMPROD1;
P4: ( dom xx1 = dom CX & dom yy1 = dom CY & dom rxx1 = dom CX & dom ryy1 = dom CY ) by CARD_3:18;
P55: I . v = I . (x1,y1) by P52
.= xx1 ^ yy1 by P1 ;
P57: I . (r * v) = I . ((r * x1),(r * y1)) by P52, defMLT
.= rxx1 ^ ryy1 by P1 ;
reconsider Iv = I . v as Element of product (carr (X ^ Y)) ;
reconsider rIv = r * (I . v) as FinSequence by LMPROD1;
XX1: dom rIv = dom (carr (X ^ Y)) by CARD_3:18;
X5: dom (rxx1 ^ ryy1) = dom (carr (X ^ Y)) by P57, CARD_3:18;
for j0 being Nat st j0 in dom rIv holds
rIv . j0 = (rxx1 ^ ryy1) . j0

proof

let j0 be Nat; :: thesis:
assume X20: j0 in dom rIv ; :: thesis:
then reconsider j = j0 as Element of dom (carr (X ^ Y)) by CARD_3:18;
X21: rIv . j0 = ((multop (X ^ Y)) . j) . (r,(Iv . j)) by PRVECT_2:def 2
.= the Mult of ((X ^ Y) . j) . (r,(Iv . j)) by PRVECT_2:def 8 ;

per cases by Q3, X20, XX1, FINSEQ_1:38;

suppose C1: j0 in dom CX ; :: thesis:

then j0 in dom X by A1, FINSEQ_3:31;
then C13: (X ^ Y) . j = X . j0 by FINSEQ_1:def 7;
C17: Iv . j = xx1 . j by C1, P4, P55, FINSEQ_1:def 7;
F16: (rxx1 ^ ryy1) . j0 = rxx1 . j0 by C1, P4, FINSEQ_1:def 7;
reconsider j1 = j0 as Element of dom (carr X) by C1;
the Mult of ((X ^ Y) . j) . (r,(Iv . j)) = ((multop X) . j1) . (r,(xx1 . j1)) by C13, C17, PRVECT_2:def 8
.= (rxx1 ^ ryy1) . j0 by F16, PRVECT_2:def 2 ;
hence rIv . j0 = (rxx1 ^ ryy1) . j0 by X21; :: thesis:

end;

suppose ex n being Nat st
( n in dom CY & j0 = (len CX) + n ) ; :: thesis:

then consider n being Nat such that
C1: ( n in dom CY & j0 = (len CX) + n ) ;
G2: ( len CX = len xx1 & len CX = len rxx1 ) by P4, FINSEQ_3:31;
n in dom Y by C1, A1, FINSEQ_3:31;
then C13: (X ^ Y) . j = Y . n by C1, A1, FINSEQ_1:def 7;
C17: Iv . j = yy1 . n by P55, C1, P4, G2, FINSEQ_1:def 7;
F16: (rxx1 ^ ryy1) . j0 = ryy1 . n by C1, G2, P4, FINSEQ_1:def 7;
reconsider j1 = n as Element of dom (carr Y) by C1;
the Mult of ((X ^ Y) . j) . (r,(Iv . j)) = ((multop Y) . j1) . (r,(yy1 . j1)) by C13, C17, PRVECT_2:def 8
.= (rxx1 ^ ryy1) . j0 by F16, PRVECT_2:def 2 ;
hence rIv . j0 = (rxx1 ^ ryy1) . j0 by X21; :: thesis:

end;

hence I . (r * v) = r * (I . v) by P57, X5, XX1, FINSEQ_1:17; :: thesis:

end;

I . (0. [:(product X),(product Y):]) = I . ((0. [:(product X),(product Y):]) + (0. [:(product X),(product Y):])) by RLVECT_1:def 7
.= (I . (0. [:(product X),(product Y):])) + (I . (0. [:(product X),(product Y):])) by P5 ;
then (I . (0. [:(product X),(product Y):])) - (I . (0. [:(product X),(product Y):])) = (I . (0. [:(product X),(product Y):])) + ((I . (0. [:(product X),(product Y):])) - (I . (0. [:(product X),(product Y):]))) by RLVECT_1:42
.= (I . (0. [:(product X),(product Y):])) + (0. (product (X ^ Y))) by RLVECT_1:28
.= I . (0. [:(product X),(product Y):]) by RLVECT_1:def 7 ;
then 0. (product (X ^ Y)) = I . (0. [:(product X),(product Y):]) by RLVECT_1:28;
hence 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)) ) by P2, P5, P6, P1, Q5; :: thesis: