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

proof

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

end;

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