let G be strict Group; :: thesis: for f being object holds
( f in InnAut G iff f is inner Automorphism of G )
let f be object ; :: thesis: ( f in InnAut G iff f is inner Automorphism of G )
A1: ( f is Automorphism of G implies f is Element of Funcs ( the carrier of G, the carrier of G) ) by FUNCT_2:9;
thus ( f in InnAut G implies f is inner Automorphism of G ) :: thesis: ( f is inner Automorphism of G implies f in InnAut G )

proof

assume B1: f in InnAut G ; :: thesis: f is inner Automorphism of G
then reconsider f = f as Automorphism of G by Lm6;
consider a being Element of G such that
B2: for x being Element of G holds f . x = x |^ a by A1, B1, AUTGROUP:def 4;
a is_inner_wrt f by B2;
hence f is inner Automorphism of G by Def2; :: thesis: verum

end;

assume f is inner Automorphism of G ; :: thesis: f in InnAut G
then reconsider f = f as inner Automorphism of G ;
ex a being Element of G st a is_inner_wrt f by Def2;
hence f in InnAut G by A1, AUTGROUP:def 4; :: thesis: verum