theorem :: GROUP_23:26

for G, K being Group
for H being Subgroup of G
for phi being Homomorphism of G,K holds phi | H = phi * (incl H)