for G, H being AddGroup
for F being strict Morphism of G,H ex f being Function of G,H st F = GroupMorphismStr(# G,H,f #)