for I being non empty set
for G being Group
for M being DirectSumComponents of G,I ex f being Homomorphism of (sum M),G ex N being internal DirectSumComponents of G,I st
( f is bijective & ( for i being Element of I ex qi being Homomorphism of (M . i),(N . i) st
( qi = f * (1ProdHom (M,i)) & qi is bijective ) ) )