let G be strict Group; :: thesis: InnAut G c= Aut G

let q be object ; :: according to TARSKI:def 3 :: thesis: ( not q in InnAut G or q in Aut G )

assume q in InnAut G ; :: thesis: q in Aut G

then consider f being Element of InnAut G such that

A1: f = q ;

f is Element of Aut G by Th12;

hence q in Aut G by A1; :: thesis: verum

let q be object ; :: according to TARSKI:def 3 :: thesis: ( not q in InnAut G or q in Aut G )

assume q in InnAut G ; :: thesis: q in Aut G

then consider f being Element of InnAut G such that

A1: f = q ;

f is Element of Aut G by Th12;

hence q in Aut G by A1; :: thesis: verum