theorem Th8: :: ALG_1:8

for U1, U2 being Universal_Algebra
for f being Function of U1,U2 st f is_isomorphism holds
( dom f = the carrier of U1 & rng f = the carrier of U2 )