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

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