theorem Th19: :: ALG_1:19

for U1, U2 being Universal_Algebra
for f being Function of U1,U2 st f is_homomorphism holds
( HomQuot f is_homomorphism & HomQuot f is_monomorphism )