let X be Group-Sequence; :: thesis:
let Y be AbGroup; :: thesis:
consider I being Homomorphism of [:(product X),Y:],[:(product X),(product <*Y*>):] such that
A1: ( I is bijective & ( for x being Element of (product X)
for y being Element of Y holds I . (x,y) = [x,<*y*>] ) ) by Th9;
consider J being Homomorphism of [:(product X),(product <*Y*>):],(product (X ^ <*Y*>)) such that
A2: ( J 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 & J . (x,y) = x1 ^ y1 ) ) ) by Th3;
set K = J * I;
reconsider K = J * I as Homomorphism of [:(product X),Y:],(product (X ^ <*Y*>)) ;
take K ; :: thesis:
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 ;
then K is onto by FUNCT_2:def 3;
hence K is bijective by A1, A2; :: thesis:
thus for x being Element of (product X)
for y being Element of Y ex x1, y1 being FinSequence st
( x = x1 & <*y*> = y1 & K . (x,y) = x1 ^ y1 ) :: thesis:

proof

let x be Element of (product X); :: thesis:
let y be Element of Y; :: thesis:
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 Element 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:

end;