theorem Th13: :: GRSOLV_1:13

for G, H being strict Group
for h being Homomorphism of G,H
for A being strict Subgroup of G
for a being Element of G holds
( (h . a) * (h .: A) = h .: (a * A) & (h .: A) * (h . a) = h .: (A * a) )