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