theorem Th1: :: GROUP_22:3

for G1, G2 being Group
for H being Subgroup of G1
for f being Homomorphism of G1,G2
for h being Element of G1 st h in H holds
(f | H) . h = f . h