let G, H be Group; :: thesis: for h being Homomorphism of G,H holds
( h is bijective iff ( rng h = the carrier of H & h is one-to-one ) )
let h be Homomorphism of G,H; :: thesis: ( h is bijective iff ( rng h = the carrier of H & h is one-to-one ) )
thus ( h is bijective implies ( rng h = the carrier of H & h is one-to-one ) ) by FUNCT_2:def 3; :: thesis: ( rng h = the carrier of H & h is one-to-one implies h is bijective )
assume ( rng h = the carrier of H & h is one-to-one ) ; :: thesis: h is bijective
hence ( h is one-to-one & h is onto ) by FUNCT_2:def 3; :: according to FUNCT_2:def 4 :: thesis: verum