let X, Y be Group-Sequence; :: thesis: ex I being Homomorphism of [:(),():],(product (X ^ Y)) st
( I is bijective & ( for x being Element of ()
for y being Element of () ex x1, y1 being FinSequence st
( x = x1 & y = y1 & I . (x,y) = x1 ^ y1 ) ) )

reconsider CX = carr X, CY = carr Y as 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 ;
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
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 ;
A6: (carr (X ^ Y)) . k = the carrier of ((X ^ Y) . k1) by PRVECT_1:def 11;
A7: k in dom (X ^ Y) by ;
per cases ( k in dom X or ex n being Nat st
( n in dom Y & k = (len X) + n ) )
by ;
suppose A8: k in dom X ; :: thesis: (carr (X ^ Y)) . k = (CX ^ CY) . k
then A9: k in dom CX by ;
reconsider k2 = k1 as Element of dom X by A8;
thus (carr (X ^ Y)) . k = the carrier of (X . k2) by
.= CX . k by PRVECT_1:def 11
.= (CX ^ CY) . k by ; :: thesis: verum
end;
suppose ex n being Nat st
( 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 ;
reconsider n1 = n as Element of dom Y by A10;
thus (carr (X ^ Y)) . k = the carrier of (Y . n1) by
.= CY . n by PRVECT_1:def 11
.= (CX ^ CY) . k by ; :: thesis: verum
end;
end;
end;
then A12: carr (X ^ Y) = CX ^ CY by ;
reconsider I = I as Function of [:(),():],(product (X ^ Y)) by ;
A13: for x being Element of ()
for y being Element of () ex x1, y1 being FinSequence st
( x = x1 & y = y1 & I . (x,y) = x1 ^ y1 )
proof
let x be Element of (); :: thesis: for y being Element of () ex x1, y1 being FinSequence st
( x = x1 & y = y1 & I . (x,y) = x1 ^ y1 )

let y be Element of (); :: 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;
for v, w being Element of [:(),():] holds I . (v + w) = (I . v) + (I . w)
proof
let v, w be Element of [:(),():]; :: thesis: I . (v + w) = (I . v) + (I . w)
consider x1 being Element of (), y1 being Element of () such that
A14: v = [x1,y1] by SUBSET_1:43;
consider x2 being Element of (), y2 being Element of () such that
A15: 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;
A16: ( 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 ;
then A17: ( I . v = xx1 ^ yy1 & I . w = xx2 ^ yy2 ) by A2;
I . (v + w) = I . ((x1 + x2),(y1 + y2)) by ;
then A18: I . (v + w) = xx12 ^ yy12 by A2;
then A19: 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
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;
A20: 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 ;
suppose A21: j0 in dom CX ; :: thesis: Ivw . j0 = (xx12 ^ yy12) . j0
then j0 in dom X by ;
then A22: (X ^ Y) . j = X . j0 by FINSEQ_1:def 7;
A23: ( Iv . j = xx1 . j & Iw . j = xx2 . j ) by ;
A24: (xx12 ^ yy12) . j0 = xx12 . j0 by ;
reconsider j1 = j0 as Element of dom (carr X) by A21;
the addF of ((X ^ Y) . j) . ((Iv . j),(Iw . j)) = (() . j1) . ((xx1 . j1),(xx2 . j1)) by
.= (xx12 ^ yy12) . j0 by ;
hence Ivw . j0 = (xx12 ^ yy12) . j0 by A20; :: thesis: verum
end;
suppose ex n being Nat st
( n in dom CY & j0 = (len CX) + n ) ; :: thesis: Ivw . j0 = (xx12 ^ yy12) . j0
then consider n being Nat such that
A25: ( n in dom CY & j0 = (len CX) + n ) ;
A26: ( len CX = len xx1 & len CX = len xx2 & len CX = len xx12 ) by ;
n in dom Y by ;
then A27: (X ^ Y) . j = Y . n by ;
A28: ( Iv . j = yy1 . n & Iw . j = yy2 . n ) by ;
A29: (xx12 ^ yy12) . j0 = yy12 . n by ;
reconsider j1 = n as Element of dom (carr Y) by A25;
the addF of ((X ^ Y) . j) . ((Iv . j),(Iw . j)) = (() . j1) . ((yy1 . j1),(yy2 . j1)) by
.= (xx12 ^ yy12) . j0 by ;
hence Ivw . j0 = (xx12 ^ yy12) . j0 by A20; :: thesis: verum
end;
end;
end;
hence I . (v + w) = (I . v) + (I . w) by ; :: thesis: verum
end;
then reconsider I = I as Homomorphism of [:(),():],(product (X ^ Y)) by VECTSP_1:def 20;
take I ; :: thesis: ( I is bijective & ( for x being Element of ()
for y being Element of () ex x1, y1 being FinSequence st
( x = x1 & y = y1 & I . (x,y) = x1 ^ y1 ) ) )

thus ( I is bijective & ( for x being Element of ()
for y being Element of () ex x1, y1 being FinSequence st
( x = x1 & y = y1 & I . (x,y) = x1 ^ y1 ) ) ) by A13, A2, A12; :: thesis: verum