let G, H be Group; 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; 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; ( rng f c= [#] H0 implies f is Homomorphism of G,H0 )
assume
rng f c= [#] H0
; 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)
hence
f is Homomorphism of G,H0
by GROUP_6:def 6; verum