let X, Y be Group-Sequence; :: thesis: ex I being Homomorphism of (product <*(),()*>),(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 ) ) )

set PX = product X;
set PY = product Y;
set PXY = product (X ^ Y);
consider K being Homomorphism of [:(),():],(product (X ^ Y)) such that
A1: ( K is bijective & ( for x being Element of ()
for y being Element of () ex x1, y1 being FinSequence st
( x = x1 & y = y1 & K . (x,y) = x1 ^ y1 ) ) ) by Th3;
consider J being Homomorphism of [:(),():],(product <*(),()*>) such that
A2: ( J is bijective & ( for x being Element of ()
for y being Element of () holds J . (x,y) = <*x,y*> ) ) by Th2;
reconsider JB = J " as Homomorphism of (product <*(),()*>),[:(),():] by ;
dom J = the carrier of [:(),():] by FUNCT_2:def 1;
then rng JB = the carrier of [:(),():] by ;
then A3: JB is onto by FUNCT_2:def 3;
reconsider I = K * JB as Homomorphism of (product <*(),()*>),(product (X ^ Y)) ;
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 ) ) )

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

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 [:(),():] ;
then A6: [x,y] in dom J by FUNCT_2:def 1;
I . <*x,y*> = K . (JB . (J . [x,y])) by ;
then I . <*x,y*> = x1 ^ y1 by ;
hence ex x1, y1 being FinSequence st
( x = x1 & y = y1 & I . <*x,y*> = x1 ^ y1 ) by A4; :: thesis: verum
end;