let K be Ring; :: thesis: for X, Y being VectorSpace-Sequence of K ex I being Function of [:(product X),(product Y):],(product (X ^ Y)) st

( I is one-to-one & I is onto & ( for x being Vector of (product X)

for y being Vector of (product Y) ex x1, y1 being FinSequence st

( x = x1 & y = y1 & I . (x,y) = x1 ^ y1 ) ) & ( for v, w being Vector of [:(product X),(product Y):] holds I . (v + w) = (I . v) + (I . w) ) & ( for v being Vector of [:(product X),(product Y):]

for r being Element of the carrier of K holds I . (r * v) = r * (I . v) ) & I . (0. [:(product X),(product Y):]) = 0. (product (X ^ Y)) )

let X, Y be VectorSpace-Sequence of K; :: thesis: ex I being Function of [:(product X),(product Y):],(product (X ^ Y)) st

( I is one-to-one & I is onto & ( for x being Vector of (product X)

for y being Vector of (product Y) ex x1, y1 being FinSequence st

( x = x1 & y = y1 & I . (x,y) = x1 ^ y1 ) ) & ( for v, w being Vector of [:(product X),(product Y):] holds I . (v + w) = (I . v) + (I . w) ) & ( for v being Vector of [:(product X),(product Y):]

for r being Element of the carrier of K holds I . (r * v) = r * (I . v) ) & I . (0. [:(product X),(product Y):]) = 0. (product (X ^ Y)) )

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_1:def 11;

consider I being Function of [:(product CX),(product CY):],(product (CX ^ CY)) such that

A2: ( 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 PRVECT_3:6;

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:22;

then A3: dom (carr (X ^ Y)) = dom (CX ^ CY) by FINSEQ_3:29;

A4: for k being Nat st k in dom (carr (X ^ Y)) holds

(carr (X ^ Y)) . k = (CX ^ CY) . k

reconsider I = I as Function of [:(product X),(product Y):],(product (X ^ Y)) by A3, A4, FINSEQ_1:13;

A13: for x being Vector of (product X)

for y being Vector of (product Y) ex x1, y1 being FinSequence st

( x = x1 & y = y1 & I . (x,y) = x1 ^ y1 )

for r being Element of the carrier of K holds I . (r * v) = r * (I . v)

.= (I . (0. [:(product X),(product Y):])) + (I . (0. [:(product X),(product Y):])) by A14 ;

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:28

.= (I . (0. [:(product X),(product Y):])) + (0. (product (X ^ Y))) by RLVECT_1:15

.= I . (0. [:(product X),(product Y):]) ;

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 Vector of (product X)

for y being Vector of (product Y) ex x1, y1 being FinSequence st

( x = x1 & y = y1 & I . (x,y) = x1 ^ y1 ) ) & ( for v, w being Vector of [:(product X),(product Y):] holds I . (v + w) = (I . v) + (I . w) ) & ( for v being Vector of [:(product X),(product Y):]

for r being Element of the carrier of K holds I . (r * v) = r * (I . v) ) & I . (0. [:(product X),(product Y):]) = 0. (product (X ^ Y)) ) by A13, A14, A32, A2, A12, RLVECT_1:15; :: thesis: verum

( I is one-to-one & I is onto & ( for x being Vector of (product X)

for y being Vector of (product Y) ex x1, y1 being FinSequence st

( x = x1 & y = y1 & I . (x,y) = x1 ^ y1 ) ) & ( for v, w being Vector of [:(product X),(product Y):] holds I . (v + w) = (I . v) + (I . w) ) & ( for v being Vector of [:(product X),(product Y):]

for r being Element of the carrier of K holds I . (r * v) = r * (I . v) ) & I . (0. [:(product X),(product Y):]) = 0. (product (X ^ Y)) )

let X, Y be VectorSpace-Sequence of K; :: thesis: ex I being Function of [:(product X),(product Y):],(product (X ^ Y)) st

( I is one-to-one & I is onto & ( for x being Vector of (product X)

for y being Vector of (product Y) ex x1, y1 being FinSequence st

( x = x1 & y = y1 & I . (x,y) = x1 ^ y1 ) ) & ( for v, w being Vector of [:(product X),(product Y):] holds I . (v + w) = (I . v) + (I . w) ) & ( for v being Vector of [:(product X),(product Y):]

for r being Element of the carrier of K holds I . (r * v) = r * (I . v) ) & I . (0. [:(product X),(product Y):]) = 0. (product (X ^ Y)) )

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_1:def 11;

consider I being Function of [:(product CX),(product CY):],(product (CX ^ CY)) such that

A2: ( 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 PRVECT_3:6;

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:22;

then A3: dom (carr (X ^ Y)) = dom (CX ^ CY) by FINSEQ_3:29;

A4: for k being Nat st k in dom (carr (X ^ Y)) holds

(carr (X ^ Y)) . k = (CX ^ CY) . k

proof

then A12:
carr (X ^ Y) = CX ^ CY
by A3, FINSEQ_1:13;
let k be Nat; :: thesis: ( k in dom (carr (X ^ Y)) implies (carr (X ^ Y)) . k = (CX ^ CY) . k )

assume A5: k in dom (carr (X ^ Y)) ; :: thesis: (carr (X ^ Y)) . k = (CX ^ CY) . k

then reconsider k1 = k as Element of dom (X ^ Y) by A1, FINSEQ_3:29;

A6: (carr (X ^ Y)) . k = the carrier of ((X ^ Y) . k1) by PRVECT_1:def 11;

A7: k in dom (X ^ Y) by A1, A5, FINSEQ_3:29;

end;assume A5: k in dom (carr (X ^ Y)) ; :: thesis: (carr (X ^ Y)) . k = (CX ^ CY) . k

then reconsider k1 = k as Element of dom (X ^ Y) by A1, FINSEQ_3:29;

A6: (carr (X ^ Y)) . k = the carrier of ((X ^ Y) . k1) by PRVECT_1:def 11;

A7: k in dom (X ^ Y) by A1, A5, FINSEQ_3:29;

per cases
( k in dom X or ex n being Nat st

( n in dom Y & k = (len X) + n ) ) by A7, FINSEQ_1:25;

end;

( n in dom Y & k = (len X) + n ) ) by A7, FINSEQ_1:25;

suppose A8:
k in dom X
; :: thesis: (carr (X ^ Y)) . k = (CX ^ CY) . k

then A9:
k in dom CX
by A1, FINSEQ_3:29;

reconsider k2 = k1 as Element of dom X by A8;

thus (carr (X ^ Y)) . k = the carrier of (X . k2) by A6, FINSEQ_1:def 7

.= CX . k by PRVECT_1:def 11

.= (CX ^ CY) . k by A9, FINSEQ_1:def 7 ; :: thesis: verum

end;reconsider k2 = k1 as Element of dom X by A8;

thus (carr (X ^ Y)) . k = the carrier of (X . k2) by A6, FINSEQ_1:def 7

.= CX . k by PRVECT_1:def 11

.= (CX ^ CY) . k by A9, FINSEQ_1:def 7 ; :: thesis: verum

suppose
ex n being Nat st

( n in dom Y & k = (len X) + n ) ; :: thesis: (carr (X ^ Y)) . k = (CX ^ CY) . k

( n in dom Y & k = (len X) + n ) ; :: thesis: (carr (X ^ Y)) . k = (CX ^ CY) . k

then consider n being Nat such that

A10: ( n in dom Y & k = (len X) + n ) ;

A11: n in dom CY by A1, A10, FINSEQ_3:29;

reconsider n1 = n as Element of dom Y by A10;

thus (carr (X ^ Y)) . k = the carrier of (Y . n1) by A6, A10, FINSEQ_1:def 7

.= CY . n by PRVECT_1:def 11

.= (CX ^ CY) . k by A11, A10, A1, FINSEQ_1:def 7 ; :: thesis: verum

end;A10: ( n in dom Y & k = (len X) + n ) ;

A11: n in dom CY by A1, A10, FINSEQ_3:29;

reconsider n1 = n as Element of dom Y by A10;

thus (carr (X ^ Y)) . k = the carrier of (Y . n1) by A6, A10, FINSEQ_1:def 7

.= CY . n by PRVECT_1:def 11

.= (CX ^ CY) . k by A11, A10, A1, FINSEQ_1:def 7 ; :: thesis: verum

reconsider I = I as Function of [:(product X),(product Y):],(product (X ^ Y)) by A3, A4, FINSEQ_1:13;

A13: for x being Vector of (product X)

for y being Vector of (product Y) ex x1, y1 being FinSequence st

( x = x1 & y = y1 & I . (x,y) = x1 ^ y1 )

proof

A14:
for v, w being Vector of [:(product X),(product Y):] holds I . (v + w) = (I . v) + (I . w)
let x be Vector of (product X); :: thesis: for y being Vector of (product Y) ex x1, y1 being FinSequence st

( x = x1 & y = y1 & I . (x,y) = x1 ^ y1 )

let y be Vector of (product Y); :: thesis: ex x1, y1 being FinSequence st

( x = x1 & y = y1 & I . (x,y) = x1 ^ y1 )

reconsider x1 = x, y1 = y as FinSequence by NDIFF_5:9;

I . (x,y) = x1 ^ y1 by A2;

hence ex x1, y1 being FinSequence st

( x = x1 & y = y1 & I . (x,y) = x1 ^ y1 ) ; :: thesis: verum

end;( x = x1 & y = y1 & I . (x,y) = x1 ^ y1 )

let y be Vector of (product Y); :: thesis: ex x1, y1 being FinSequence st

( x = x1 & y = y1 & I . (x,y) = x1 ^ y1 )

reconsider x1 = x, y1 = y as FinSequence by NDIFF_5:9;

I . (x,y) = x1 ^ y1 by A2;

hence ex x1, y1 being FinSequence st

( x = x1 & y = y1 & I . (x,y) = x1 ^ y1 ) ; :: thesis: verum

proof

A32:
for v being Vector of [:(product X),(product Y):]
let v, w be Vector of [:(product X),(product Y):]; :: thesis: I . (v + w) = (I . v) + (I . w)

consider x1 being Vector of (product X), y1 being Vector of (product Y) such that

A15: v = [x1,y1] by SUBSET_1:43;

consider x2 being Vector of (product X), y2 being Vector of (product Y) such that

A16: w = [x2,y2] by SUBSET_1:43;

reconsider xx1 = x1, xx2 = x2 as FinSequence by NDIFF_5:9;

reconsider yy1 = y1, yy2 = y2 as FinSequence by NDIFF_5:9;

reconsider xx12 = x1 + x2, yy12 = y1 + y2 as FinSequence by NDIFF_5:9;

A17: ( 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:9;

( I . v = I . (x1,y1) & I . w = I . (x2,y2) ) by A15, A16;

then A18: ( I . v = xx1 ^ yy1 & I . w = xx2 ^ yy2 ) by A2;

I . (v + w) = I . ((x1 + x2),(y1 + y2)) by A15, A16, PRVECT_3:def 1;

then A19: I . (v + w) = xx12 ^ yy12 by A2;

then A20: dom (xx12 ^ yy12) = dom (carr (X ^ Y)) by CARD_3:9;

reconsider Iv = I . v, Iw = I . w as Element of product (carr (X ^ Y)) ;

reconsider Ivw = (I . v) + (I . w) as FinSequence by NDIFF_5:9;

for j0 being Nat st j0 in dom Ivw holds

Ivw . j0 = (xx12 ^ yy12) . j0

end;consider x1 being Vector of (product X), y1 being Vector of (product Y) such that

A15: v = [x1,y1] by SUBSET_1:43;

consider x2 being Vector of (product X), y2 being Vector of (product Y) such that

A16: w = [x2,y2] by SUBSET_1:43;

reconsider xx1 = x1, xx2 = x2 as FinSequence by NDIFF_5:9;

reconsider yy1 = y1, yy2 = y2 as FinSequence by NDIFF_5:9;

reconsider xx12 = x1 + x2, yy12 = y1 + y2 as FinSequence by NDIFF_5:9;

A17: ( 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:9;

( I . v = I . (x1,y1) & I . w = I . (x2,y2) ) by A15, A16;

then A18: ( I . v = xx1 ^ yy1 & I . w = xx2 ^ yy2 ) by A2;

I . (v + w) = I . ((x1 + x2),(y1 + y2)) by A15, A16, PRVECT_3:def 1;

then A19: I . (v + w) = xx12 ^ yy12 by A2;

then A20: dom (xx12 ^ yy12) = dom (carr (X ^ Y)) by CARD_3:9;

reconsider Iv = I . v, Iw = I . w as Element of product (carr (X ^ Y)) ;

reconsider Ivw = (I . v) + (I . w) as FinSequence by NDIFF_5:9;

for j0 being Nat st j0 in dom Ivw holds

Ivw . j0 = (xx12 ^ yy12) . j0

proof

hence
I . (v + w) = (I . v) + (I . w)
by A19, A20, CARD_3:9, FINSEQ_1:13; :: thesis: verum
let j0 be Nat; :: thesis: ( j0 in dom Ivw implies Ivw . j0 = (xx12 ^ yy12) . j0 )

assume j0 in dom Ivw ; :: thesis: Ivw . j0 = (xx12 ^ yy12) . j0

then reconsider j = j0 as Element of dom (carr (X ^ Y)) by CARD_3:9;

A22: Ivw . j0 = ((addop (X ^ Y)) . j) . ((Iv . j),(Iw . j)) by PRVECT_1:def 8

.= the addF of ((X ^ Y) . j) . ((Iv . j),(Iw . j)) by PRVECT_1:def 12 ;

end;assume j0 in dom Ivw ; :: thesis: Ivw . j0 = (xx12 ^ yy12) . j0

then reconsider j = j0 as Element of dom (carr (X ^ Y)) by CARD_3:9;

A22: Ivw . j0 = ((addop (X ^ Y)) . j) . ((Iv . j),(Iw . j)) by PRVECT_1:def 8

.= the addF of ((X ^ Y) . j) . ((Iv . j),(Iw . j)) by PRVECT_1:def 12 ;

per cases
( j0 in dom CX or ex n being Nat st

( n in dom CY & j0 = (len CX) + n ) ) by A22, A3, FINSEQ_1:25;

end;

( n in dom CY & j0 = (len CX) + n ) ) by A22, A3, FINSEQ_1:25;

suppose A23:
j0 in dom CX
; :: thesis: Ivw . j0 = (xx12 ^ yy12) . j0

then
j0 in dom X
by A1, FINSEQ_3:29;

then A24: (X ^ Y) . j = X . j0 by FINSEQ_1:def 7;

A25: ( Iv . j = xx1 . j & Iw . j = xx2 . j ) by A23, A17, A18, FINSEQ_1:def 7;

A26: (xx12 ^ yy12) . j0 = xx12 . j0 by A23, A17, FINSEQ_1:def 7;

reconsider j1 = j0 as Element of dom (carr X) by A23;

the addF of ((X ^ Y) . j) . ((Iv . j),(Iw . j)) = ((addop X) . j1) . ((xx1 . j1),(xx2 . j1)) by A24, A25, PRVECT_1:def 12

.= (xx12 ^ yy12) . j0 by A26, PRVECT_1:def 8 ;

hence Ivw . j0 = (xx12 ^ yy12) . j0 by A22; :: thesis: verum

end;then A24: (X ^ Y) . j = X . j0 by FINSEQ_1:def 7;

A25: ( Iv . j = xx1 . j & Iw . j = xx2 . j ) by A23, A17, A18, FINSEQ_1:def 7;

A26: (xx12 ^ yy12) . j0 = xx12 . j0 by A23, A17, FINSEQ_1:def 7;

reconsider j1 = j0 as Element of dom (carr X) by A23;

the addF of ((X ^ Y) . j) . ((Iv . j),(Iw . j)) = ((addop X) . j1) . ((xx1 . j1),(xx2 . j1)) by A24, A25, PRVECT_1:def 12

.= (xx12 ^ yy12) . j0 by A26, PRVECT_1:def 8 ;

hence Ivw . j0 = (xx12 ^ yy12) . j0 by A22; :: thesis: verum

suppose
ex n being Nat st

( n in dom CY & j0 = (len CX) + n ) ; :: thesis: Ivw . j0 = (xx12 ^ yy12) . j0

( n in dom CY & j0 = (len CX) + n ) ; :: thesis: Ivw . j0 = (xx12 ^ yy12) . j0

then consider n being Nat such that

A27: ( n in dom CY & j0 = (len CX) + n ) ;

A28: ( len CX = len xx1 & len CX = len xx2 & len CX = len xx12 ) by A17, FINSEQ_3:29;

n in dom Y by A1, A27, FINSEQ_3:29;

then A29: (X ^ Y) . j = Y . n by A27, A1, FINSEQ_1:def 7;

A30: ( Iv . j = yy1 . n & Iw . j = yy2 . n ) by A17, A18, A27, A28, FINSEQ_1:def 7;

A31: (xx12 ^ yy12) . j0 = yy12 . n by A27, A28, A17, FINSEQ_1:def 7;

reconsider j1 = n as Element of dom (carr Y) by A27;

the addF of ((X ^ Y) . j) . ((Iv . j),(Iw . j)) = ((addop Y) . j1) . ((yy1 . j1),(yy2 . j1)) by A29, A30, PRVECT_1:def 12

.= (xx12 ^ yy12) . j0 by A31, PRVECT_1:def 8 ;

hence Ivw . j0 = (xx12 ^ yy12) . j0 by A22; :: thesis: verum

end;A27: ( n in dom CY & j0 = (len CX) + n ) ;

A28: ( len CX = len xx1 & len CX = len xx2 & len CX = len xx12 ) by A17, FINSEQ_3:29;

n in dom Y by A1, A27, FINSEQ_3:29;

then A29: (X ^ Y) . j = Y . n by A27, A1, FINSEQ_1:def 7;

A30: ( Iv . j = yy1 . n & Iw . j = yy2 . n ) by A17, A18, A27, A28, FINSEQ_1:def 7;

A31: (xx12 ^ yy12) . j0 = yy12 . n by A27, A28, A17, FINSEQ_1:def 7;

reconsider j1 = n as Element of dom (carr Y) by A27;

the addF of ((X ^ Y) . j) . ((Iv . j),(Iw . j)) = ((addop Y) . j1) . ((yy1 . j1),(yy2 . j1)) by A29, A30, PRVECT_1:def 12

.= (xx12 ^ yy12) . j0 by A31, PRVECT_1:def 8 ;

hence Ivw . j0 = (xx12 ^ yy12) . j0 by A22; :: thesis: verum

for r being Element of the carrier of K holds I . (r * v) = r * (I . v)

proof

I . (0. [:(product X),(product Y):]) =
I . ((0. [:(product X),(product Y):]) + (0. [:(product X),(product Y):]))
let v be Vector of [:(product X),(product Y):]; :: thesis: for r being Element of the carrier of K holds I . (r * v) = r * (I . v)

let r be Element of the carrier of K; :: thesis: I . (r * v) = r * (I . v)

consider x1 being Vector of (product X), y1 being Vector of (product Y) such that

A33: v = [x1,y1] by SUBSET_1:43;

reconsider xx1 = x1, yy1 = y1 as FinSequence by NDIFF_5:9;

reconsider rxx1 = r * x1, ryy1 = r * y1 as FinSequence by NDIFF_5:9;

A34: ( dom xx1 = dom CX & dom yy1 = dom CY & dom rxx1 = dom CX & dom ryy1 = dom CY ) by CARD_3:9;

A35: I . v = I . (x1,y1) by A33

.= xx1 ^ yy1 by A2 ;

A36: I . (r * v) = I . ((r * x1),(r * y1)) by A33, YDef2

.= rxx1 ^ ryy1 by A2 ;

reconsider Iv = I . v as Element of product (carr (X ^ Y)) ;

reconsider rIv = r * (I . v) as FinSequence by NDIFF_5:9;

A37: dom rIv = dom (carr (X ^ Y)) by CARD_3:9;

A38: dom (rxx1 ^ ryy1) = dom (carr (X ^ Y)) by A36, CARD_3:9;

for j0 being Nat st j0 in dom rIv holds

rIv . j0 = (rxx1 ^ ryy1) . j0

end;let r be Element of the carrier of K; :: thesis: I . (r * v) = r * (I . v)

consider x1 being Vector of (product X), y1 being Vector of (product Y) such that

A33: v = [x1,y1] by SUBSET_1:43;

reconsider xx1 = x1, yy1 = y1 as FinSequence by NDIFF_5:9;

reconsider rxx1 = r * x1, ryy1 = r * y1 as FinSequence by NDIFF_5:9;

A34: ( dom xx1 = dom CX & dom yy1 = dom CY & dom rxx1 = dom CX & dom ryy1 = dom CY ) by CARD_3:9;

A35: I . v = I . (x1,y1) by A33

.= xx1 ^ yy1 by A2 ;

A36: I . (r * v) = I . ((r * x1),(r * y1)) by A33, YDef2

.= rxx1 ^ ryy1 by A2 ;

reconsider Iv = I . v as Element of product (carr (X ^ Y)) ;

reconsider rIv = r * (I . v) as FinSequence by NDIFF_5:9;

A37: dom rIv = dom (carr (X ^ Y)) by CARD_3:9;

A38: dom (rxx1 ^ ryy1) = dom (carr (X ^ Y)) by A36, CARD_3:9;

for j0 being Nat st j0 in dom rIv holds

rIv . j0 = (rxx1 ^ ryy1) . j0

proof

hence
I . (r * v) = r * (I . v)
by A36, A38, CARD_3:9, FINSEQ_1:13; :: thesis: verum
let j0 be Nat; :: thesis: ( j0 in dom rIv implies rIv . j0 = (rxx1 ^ ryy1) . j0 )

assume A39: j0 in dom rIv ; :: thesis: rIv . j0 = (rxx1 ^ ryy1) . j0

then reconsider j = j0 as Element of dom (carr (X ^ Y)) by CARD_3:9;

A40: rIv . j0 = ((multop (X ^ Y)) . j) . (r,(Iv . j)) by PRVECT_2:def 2

.= the lmult of ((X ^ Y) . j) . (r,(Iv . j)) by Def8 ;

end;assume A39: j0 in dom rIv ; :: thesis: rIv . j0 = (rxx1 ^ ryy1) . j0

then reconsider j = j0 as Element of dom (carr (X ^ Y)) by CARD_3:9;

A40: rIv . j0 = ((multop (X ^ Y)) . j) . (r,(Iv . j)) by PRVECT_2:def 2

.= the lmult of ((X ^ Y) . j) . (r,(Iv . j)) by Def8 ;

per cases
( j0 in dom CX or ex n being Nat st

( n in dom CY & j0 = (len CX) + n ) ) by A3, A39, A37, FINSEQ_1:25;

end;

( n in dom CY & j0 = (len CX) + n ) ) by A3, A39, A37, FINSEQ_1:25;

suppose A41:
j0 in dom CX
; :: thesis: rIv . j0 = (rxx1 ^ ryy1) . j0

then
j0 in dom X
by A1, FINSEQ_3:29;

then A42: (X ^ Y) . j = X . j0 by FINSEQ_1:def 7;

A43: Iv . j = xx1 . j by A41, A34, A35, FINSEQ_1:def 7;

A44: (rxx1 ^ ryy1) . j0 = rxx1 . j0 by A41, A34, FINSEQ_1:def 7;

reconsider j1 = j0 as Element of dom (carr X) by A41;

the lmult of ((X ^ Y) . j) . (r,(Iv . j)) = ((multop X) . j1) . (r,(xx1 . j1)) by A42, A43, Def8

.= (rxx1 ^ ryy1) . j0 by A44, PRVECT_2:def 2 ;

hence rIv . j0 = (rxx1 ^ ryy1) . j0 by A40; :: thesis: verum

end;then A42: (X ^ Y) . j = X . j0 by FINSEQ_1:def 7;

A43: Iv . j = xx1 . j by A41, A34, A35, FINSEQ_1:def 7;

A44: (rxx1 ^ ryy1) . j0 = rxx1 . j0 by A41, A34, FINSEQ_1:def 7;

reconsider j1 = j0 as Element of dom (carr X) by A41;

the lmult of ((X ^ Y) . j) . (r,(Iv . j)) = ((multop X) . j1) . (r,(xx1 . j1)) by A42, A43, Def8

.= (rxx1 ^ ryy1) . j0 by A44, PRVECT_2:def 2 ;

hence rIv . j0 = (rxx1 ^ ryy1) . j0 by A40; :: thesis: verum

suppose
ex n being Nat st

( n in dom CY & j0 = (len CX) + n ) ; :: thesis: rIv . j0 = (rxx1 ^ ryy1) . j0

( n in dom CY & j0 = (len CX) + n ) ; :: thesis: rIv . j0 = (rxx1 ^ ryy1) . j0

then consider n being Nat such that

A45: ( n in dom CY & j0 = (len CX) + n ) ;

A46: ( len CX = len xx1 & len CX = len rxx1 ) by A34, FINSEQ_3:29;

n in dom Y by A45, A1, FINSEQ_3:29;

then A47: (X ^ Y) . j = Y . n by A45, A1, FINSEQ_1:def 7;

A48: Iv . j = yy1 . n by A35, A45, A34, A46, FINSEQ_1:def 7;

A49: (rxx1 ^ ryy1) . j0 = ryy1 . n by A45, A46, A34, FINSEQ_1:def 7;

reconsider j1 = n as Element of dom (carr Y) by A45;

the lmult of ((X ^ Y) . j) . (r,(Iv . j)) = ((multop Y) . j1) . (r,(yy1 . j1)) by A47, A48, Def8

.= (rxx1 ^ ryy1) . j0 by A49, PRVECT_2:def 2 ;

hence rIv . j0 = (rxx1 ^ ryy1) . j0 by A40; :: thesis: verum

end;A45: ( n in dom CY & j0 = (len CX) + n ) ;

A46: ( len CX = len xx1 & len CX = len rxx1 ) by A34, FINSEQ_3:29;

n in dom Y by A45, A1, FINSEQ_3:29;

then A47: (X ^ Y) . j = Y . n by A45, A1, FINSEQ_1:def 7;

A48: Iv . j = yy1 . n by A35, A45, A34, A46, FINSEQ_1:def 7;

A49: (rxx1 ^ ryy1) . j0 = ryy1 . n by A45, A46, A34, FINSEQ_1:def 7;

reconsider j1 = n as Element of dom (carr Y) by A45;

the lmult of ((X ^ Y) . j) . (r,(Iv . j)) = ((multop Y) . j1) . (r,(yy1 . j1)) by A47, A48, Def8

.= (rxx1 ^ ryy1) . j0 by A49, PRVECT_2:def 2 ;

hence rIv . j0 = (rxx1 ^ ryy1) . j0 by A40; :: thesis: verum

.= (I . (0. [:(product X),(product Y):])) + (I . (0. [:(product X),(product Y):])) by A14 ;

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:28

.= (I . (0. [:(product X),(product Y):])) + (0. (product (X ^ Y))) by RLVECT_1:15

.= I . (0. [:(product X),(product Y):]) ;

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 Vector of (product X)

for y being Vector of (product Y) ex x1, y1 being FinSequence st

( x = x1 & y = y1 & I . (x,y) = x1 ^ y1 ) ) & ( for v, w being Vector of [:(product X),(product Y):] holds I . (v + w) = (I . v) + (I . w) ) & ( for v being Vector of [:(product X),(product Y):]

for r being Element of the carrier of K holds I . (r * v) = r * (I . v) ) & I . (0. [:(product X),(product Y):]) = 0. (product (X ^ Y)) ) by A13, A14, A32, A2, A12, RLVECT_1:15; :: thesis: verum