for X, Y being Group-Sequence ex I being Homomorphism of [:(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 ) ) )