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

( I 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 & I . <*x,y*> = x1 ^ y1 ) ) )

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 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 & I . <*x,y*> = x1 ^ y1 ) ) )

I is onto by A1, A3, FUNCT_2:27;

hence I is bijective by A1, A2; :: thesis: 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 )

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

( I 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 & I . <*x,y*> = x1 ^ y1 ) ) )

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 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 & I . <*x,y*> = x1 ^ y1 ) ) )

I is onto by A1, A3, FUNCT_2:27;

hence I is bijective by A1, A2; :: thesis: 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 )

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

proof

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

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

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

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

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

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

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

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

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