let X, Y be Group-Sequence; :: thesis:
set PX = product X;
set PY = product Y;
set PXY = product (X ^ Y);
consider K being Homomorphism of [:(product X),(product Y):],(product (X ^ Y)) such that
A1: ( K is bijective & ( for x being Element of (product X)
for y being Element of (product Y) ex x1, y1 being FinSequence st
( x = x1 & y = y1 & K . (x,y) = x1 ^ y1 ) ) ) by Th3;
consider J being Homomorphism of [:(product X),(product Y):],(product <*(product X),(product Y)*>) such that
A2: ( J is bijective & ( for x being Element of (product X)
for y being Element of (product Y) holds J . (x,y) = <*x,y*> ) ) by Th2;
reconsider JB = J " as Homomorphism of (product <*(product X),(product Y)*>),[:(product X),(product Y):] by A2, Th7;
dom J = the carrier of [:(product X),(product Y):] by FUNCT_2:def 1;
then rng JB = the carrier of [:(product X),(product Y):] by A2, FUNCT_1:33;
then A3: JB is onto by FUNCT_2:def 3;
reconsider I = K * JB as Homomorphism of (product <*(product X),(product Y)*>),(product (X ^ Y)) ;
take I ; :: thesis:
I is onto by A1, A3, FUNCT_2:27;
hence I is bijective by A1, A2; :: thesis:
thus for x being Element of (product X)
for y being Element of (product Y) ex x1, y1 being FinSequence st
( x = x1 & y = y1 & I . <*x,y*> = x1 ^ y1 ) :: thesis:

proof

let x be Element of (product X); :: thesis:
let y be Element of (product Y); :: thesis:
consider x1, y1 being FinSequence such that
A4: ( x = x1 & y = y1 & K . (x,y) = x1 ^ y1 ) by A1;
A5: J . (x,y) = <*x,y*> by A2;
[x,y] in the carrier of [:(product X),(product Y):] ;
then A6: [x,y] in dom J by FUNCT_2:def 1;
I . <*x,y*> = K . (JB . (J . [x,y])) by A5, FUNCT_2:15;
then I . <*x,y*> = x1 ^ y1 by A4, A6, A2, FUNCT_1:34;
hence ex x1, y1 being FinSequence st
( x = x1 & y = y1 & I . <*x,y*> = x1 ^ y1 ) by A4; :: thesis:

end;