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