let F be GroupMorphism; :: thesis: ex G, H being AddGroup st F is Morphism of G,H
take G = the Source of F; :: thesis: ex H being AddGroup st F is Morphism of G,H
take H = the Target of F; :: thesis: F is Morphism of G,H
( dom F = G & cod F = H ) ;
hence F is Morphism of G,H by Def12; :: thesis: verum