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)

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

hence
f | the carrier of H is Homomorphism of H,F
by GROUP_6:def 6; :: thesis: verum
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;( 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