let G, H be Group; :: thesis: for I being Subgroup of H
for f being Homomorphism of G,I holds f is Homomorphism of G,H
let I be Subgroup of H; :: thesis: for f being Homomorphism of G,I holds f is Homomorphism of G,H
let f be Homomorphism of G,I; :: thesis: f is Homomorphism of G,H
[#] I c= [#] H by GROUP_2:def 5;
then reconsider g = f as Function of G,H by FUNCT_2:7;

now :: thesis: for a, b being Element of G holds g . (a * b) = (g . a) * (g . b)

let a, b be Element of G; :: thesis: g . (a * b) = (g . a) * (g . b)
thus g . (a * b) = (f . a) * (f . b) by GROUP_6:def 6
.= (g . a) * (g . b) by GROUP_2:43 ; :: thesis: verum

end;

hence f is Homomorphism of G,H by GROUP_6:def 6; :: thesis: verum