let U1, U2 be Universal_Algebra; :: thesis: for f being Function of U1,U2 holds
( f is_isomorphism iff ( f is_homomorphism & rng f = the carrier of U2 & f is one-to-one ) )
let f be Function of U1,U2; :: thesis: ( f is_isomorphism iff ( f is_homomorphism & rng f = the carrier of U2 & f is one-to-one ) )
thus ( f is_isomorphism implies ( f is_homomorphism & rng f = the carrier of U2 & f is one-to-one ) ) :: thesis: ( f is_homomorphism & rng f = the carrier of U2 & f is one-to-one implies f is_isomorphism )

proof

assume f is_isomorphism ; :: thesis: ( f is_homomorphism & rng f = the carrier of U2 & f is one-to-one )
then ( f is_monomorphism & f is_epimorphism ) ;
hence ( f is_homomorphism & rng f = the carrier of U2 & f is one-to-one ) ; :: thesis: verum

end;

assume ( f is_homomorphism & rng f = the carrier of U2 & f is one-to-one ) ; :: thesis: f is_isomorphism
then ( f is_monomorphism & f is_epimorphism ) ;
hence f is_isomorphism ; :: thesis: verum