let G be Group; :: thesis: InnAut G c= Funcs ( the carrier of G, the carrier of G)
let q be object ; :: 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:9; :: thesis: verum