let G be Group; :: thesis: Aut ((1). G) = {(id ((1). G))}
for x being object st x in {(id ((1). G))} holds
x in Aut ((1). G)

proof

let x be object ; :: thesis: ( x in {(id ((1). G))} implies x in Aut ((1). G) )
assume x in {(id ((1). G))} ; :: thesis: x in Aut ((1). G)
then x = id the carrier of ((1). G) by TARSKI:def 1;
then x is Element of Aut ((1). G) by AUTGROUP:3;
hence x in Aut ((1). G) ; :: thesis: verum

end;

then A1: {(id ((1). G))} c= Aut ((1). G) ;
for x being object st x in Aut ((1). G) holds
x in {(id ((1). G))}

proof

let x be object ; :: thesis: ( x in Aut ((1). G) implies x in {(id ((1). G))} )
assume x in Aut ((1). G) ; :: thesis: x in {(id ((1). G))}
then reconsider phi = x as Homomorphism of ((1). G),((1). G) by AUTGROUP:def 1;
for g being Element of ((1). G) holds (id ((1). G)) . g = phi . g

proof

let g be Element of ((1). G); :: thesis: (id ((1). G)) . g = phi . g
g in (1). G ;
then g in {(1_ G)} by GROUP_2:def 7;
then A2: g = 1_ G by TARSKI:def 1;
hence phi . g = phi . (1_ ((1). G)) by GROUP_2:44
.= 1_ ((1). G) by GROUP_6:31
.= 1_ G by GROUP_2:44
.= (id ((1). G)) . g by A2 ;
:: thesis: verum

end;

then id ((1). G) = x by FUNCT_2:def 8;
hence x in {(id ((1). G))} by TARSKI:def 1; :: thesis: verum

end;

then Aut ((1). G) c= {(id ((1). G))} ;
hence Aut ((1). G) = {(id ((1). G))} by A1, XBOOLE_0:def 10; :: thesis: verum