theorem Th7: :: ALG_1:7

for U1, U2 being Universal_Algebra
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 ) )