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 )
f is_isomorphism UA,UA by Def1;
then ( dom f = the carrier of UA & rng f = the carrier of UA ) by ALG_1:9;
hence ( dom f = rng f & dom f = the carrier of UA ) ; :: thesis: verum