let G be strict 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

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