for X, Y being Group-Sequence 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 ) ) )