theorem Th13: :: GRCAT_1:13

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 #)