theorem Th17: :: GRCAT_1:17

for G1, G2, G3 being AddGroup
for G being Morphism of G2,G3
for F being Morphism of G1,G2 holds G * F is Morphism of G1,G3