theorem Th9: :: GRCAT_1:9

for F being GroupMorphism holds the Fun of F is additive