theorem :: GROUP_23:25

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