theorem :: GROUP_14:10

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