let G, H be Group; :: thesis: for H0 being Subgroup of H
for f being Homomorphism of G,H st rng f c= [#] H0 holds
f is Homomorphism of G,H0
let H0 be Subgroup of H; :: thesis: for f being Homomorphism of G,H st rng f c= [#] H0 holds
f is Homomorphism of G,H0
let f be Homomorphism of G,H; :: thesis: ( rng f c= [#] H0 implies f is Homomorphism of G,H0 )
assume rng f c= [#] H0 ; :: thesis: f is Homomorphism of G,H0
then reconsider g = f as Function of G,H0 by FUNCT_2:6;
for a, b being Element of G holds g . (a * b) = (g . a) * (g . b)

proof

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

end;

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