let G, F be Group; :: thesis: 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; :: thesis: 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; :: thesis: 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)

proof

let a, b be Element of H; :: thesis: g . (a * b) = (g . a) * (g . b)
( a in G & b in G ) by STRUCT_0:def 5, GROUP_2:40;
then reconsider a0 = a, b0 = b as Element of G ;
A4: f . a0 = g . a by FUNCT_1:49;
A5: f . b0 = g . b by FUNCT_1:49;
a * b = a0 * b0 by GROUP_2:43;
hence g . (a * b) = f . (a0 * b0) by FUNCT_1:49
.= (g . a) * (g . b) by GROUP_6:def 6, A4, A5 ;
:: thesis: verum

end;

hence f | the carrier of H is Homomorphism of H,F by GROUP_6:def 6; :: thesis: verum