theorem Th24: :: GRNILP_1:24

for G, H being strict Group
for h being Homomorphism of G,H
for A being strict Subgroup of G
for a, b being Element of G
for H1 being Subgroup of Image h
for a1, b1 being Element of (Image h) st a1 = h . a & b1 = h . b & H1 = h .: A holds
(a1 * b1) * H1 = ((h . a) * (h . b)) * (h .: A)