theorem Th9: :: GROUP_14:9

for X, Y being AbGroup ex I being Homomorphism of [:X,Y:],[:X,(product <*Y*>):] st
( I is bijective & ( for x being Element of X
for y being Element of Y holds I . (x,y) = [x,<*y*>] ) )