theorem Th47: :: GROUP_22:45

for G1, G2 being Group
for H being Subgroup of G1
for a being Element of G1
for f being Homomorphism of G1,G2 holds f .: (a * H) = (f . a) * (f .: H)