let U1 be Universal_Algebra; :: thesis: for U2 being strict Universal_Algebra
for f being Function of U1,U2 st f is_homomorphism holds
( f is_epimorphism iff Image f = U2 )
let U2 be strict Universal_Algebra; :: thesis: for f being Function of U1,U2 st f is_homomorphism holds
( f is_epimorphism iff Image f = U2 )
let f be Function of U1,U2; :: thesis: ( f is_homomorphism implies ( f is_epimorphism iff Image f = U2 ) )
assume A1: f is_homomorphism ; :: thesis: ( f is_epimorphism iff Image f = U2 )
thus ( f is_epimorphism implies Image f = U2 ) :: thesis: ( Image f = U2 implies f is_epimorphism )

proof

reconsider B = the carrier of (Image f) as non empty Subset of U2 by UNIALG_2:def 7;
assume f is_epimorphism ; :: thesis: Image f = U2
then A2: the carrier of U2 = rng f
.= f .: (dom f) by RELAT_1:113
.= f .: the carrier of U1 by FUNCT_2:def 1
.= the carrier of (Image f) by A1, Def6 ;
the charact of (Image f) = Opers (U2,B) by UNIALG_2:def 7;
hence Image f = U2 by A2, Th1; :: thesis: verum

end;

assume Image f = U2 ; :: thesis: f is_epimorphism
then the carrier of U2 = f .: the carrier of U1 by A1, Def6
.= f .: (dom f) by FUNCT_2:def 1
.= rng f by RELAT_1:113 ;
hence f is_epimorphism by A1; :: thesis: verum