theorem Th13: :: RING_EMB:13
for A, B being AbGroup
for i being Homomorphism of A,B st i = id A holds
A is SubAbGr of B