theorem Th20: :: GRCAT_1:20

for f, g being strict GroupMorphism st dom g = cod f holds
( dom (g * f) = dom f & cod (g * f) = cod g )