let X be Group-Sequence; :: thesis: for Y being AbGroup ex I being Homomorphism of [:(product X),Y:],(product (X ^ <*Y*>)) st

( I is bijective & ( for x being Element of (product X)

for y being Element of Y ex x1, y1 being FinSequence st

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

let Y be AbGroup; :: thesis: ex I being Homomorphism of [:(product X),Y:],(product (X ^ <*Y*>)) st

( I is bijective & ( for x being Element of (product X)

for y being Element of Y ex x1, y1 being FinSequence st

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

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: ( K is bijective & ( 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 ) ) )

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

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

( I is bijective & ( for x being Element of (product X)

for y being Element of Y ex x1, y1 being FinSequence st

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

let Y be AbGroup; :: thesis: ex I being Homomorphism of [:(product X),Y:],(product (X ^ <*Y*>)) st

( I is bijective & ( for x being Element of (product X)

for y being Element of Y ex x1, y1 being FinSequence st

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

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: ( K is bijective & ( 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 ) ) )

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

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

proof

let x be Element of (product X); :: thesis: for y being Element of Y ex x1, y1 being FinSequence st

( x = x1 & <*y*> = y1 & K . (x,y) = x1 ^ y1 )

let y be Element of Y; :: thesis: ex x1, y1 being FinSequence st

( x = x1 & <*y*> = y1 & K . (x,y) = x1 ^ y1 )

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

end;( x = x1 & <*y*> = y1 & K . (x,y) = x1 ^ y1 )

let y be Element of Y; :: thesis: ex x1, y1 being FinSequence st

( x = x1 & <*y*> = y1 & K . (x,y) = x1 ^ y1 )

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