let G, H be set ; :: thesis: for h being Function of G,H holds
( h is bijective iff ( rng h = H & h is one-to-one ) )
let h be Function of G,H; :: thesis: ( h is bijective iff ( rng h = H & h is one-to-one ) )
thus ( h is bijective implies ( rng h = H & h is one-to-one ) ) by FUNCT_2:def 3; :: thesis: ( rng h = H & h is one-to-one implies h is bijective )
assume ( rng h = 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