let G be strict Group; :: thesis: InnAut G c= Funcs the carrier of G,the carrier of G
let q be set ; :: according to TARSKI:def 3 :: thesis: ( not q in InnAut G or q in Funcs the carrier of G,the carrier of G )
assume q in InnAut G ; :: thesis: q in Funcs the carrier of G,the carrier of G
then ex f being Element of InnAut G st f = q ;
hence q in Funcs the carrier of G,the carrier of G by FUNCT_2:12; :: thesis: verum