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