for F being GroupMorphism ex G, H being AddGroup st F is Morphism of G,H