let UA be Universal_Algebra; :: thesis: for f being Element of UAAut UA holds
( dom f = rng f & dom f = the carrier of UA )
let f be Element of UAAut UA; :: thesis: ( dom f = rng f & dom f = the carrier of UA )
A1: f is_isomorphism by Def1;
then dom f = the carrier of UA by ALG_1:8;
hence ( dom f = rng f & dom f = the carrier of UA ) by A1, ALG_1:8; :: thesis: verum