let G, F be Group; for H being Subgroup of G
for f being Homomorphism of G,F holds f | the carrier of H is Homomorphism of H,F
let H be Subgroup of G; for f being Homomorphism of G,F holds f | the carrier of H is Homomorphism of H,F
let f be Homomorphism of G,F; f | the carrier of H is Homomorphism of H,F
the carrier of H c= the carrier of G
by GROUP_2:def 5;
then reconsider g = f | the carrier of H as Function of the carrier of H, the carrier of F by FUNCT_2:32;
for a, b being Element of H holds g . (a * b) = (g . a) * (g . b)
hence
f | the carrier of H is Homomorphism of H,F
by GROUP_6:def 6; verum