theorem Th25: :: GRCAT_1:25

for D being non empty set
for G, H being AddGroup holds
( D is GroupMorphism_DOMAIN of G,H iff for x being Element of D holds x is strict Morphism of G,H )