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

proof

reconsider B = the carrier of (Image f) as non empty Subset of U2 by UNIALG_2:def 8;
assume f is_epimorphism U1,U2 ; :: thesis: Image f = U2
then A2: the carrier of U2 = rng f by Def3
.= f .: (dom f) by RELAT_1:146
.= 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 8;
hence Image f = U2 by A2, Th2; :: thesis: verum

end;

assume Image f = U2 ; :: thesis: f is_epimorphism U1,U2
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:146 ;
hence f is_epimorphism U1,U2 by A1, Def3; :: thesis: verum