let G be strict Group; :: thesis: Aut G c= Funcs the carrier of G,the carrier of G
let q be set ; :: 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:12; :: thesis: verum