theorem Th23: :: GRNILP_1:23

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 holds
( ((h . a) * (h . b)) * (h .: A) = h .: ((a * b) * A) & ((h .: A) * (h . a)) * (h . b) = h .: ((A * a) * b) )