let G be Group; :: thesis: for H being strict Subgroup of G holds
( H is normal iff for f being inner Automorphism of G holds Image (f | H) = H )
let H be strict Subgroup of G; :: thesis: ( H is normal iff for f being inner Automorphism of G holds Image (f | H) = H )
thus ( H is normal implies for f being inner Automorphism of G holds Image (f | H) = H ) :: thesis: ( ( for f being inner Automorphism of G holds Image (f | H) = H ) implies H is normal )

proof

assume B1: H is normal ; :: thesis: for f being inner Automorphism of G holds Image (f | H) = H
let f be inner Automorphism of G; :: thesis: Image (f | H) = H
consider a being Element of G such that
B2: a is_inner_wrt f by Def2;
Image (f | H) = H |^ a by B2, Th28
.= multMagma(# the carrier of H, the multF of H #) by B1, GROUP_3:def 13
.= H ;
hence Image (f | H) = H ; :: thesis: verum

end;

assume B1: for f being inner Automorphism of G holds Image (f | H) = H ; :: thesis: H is normal
assume not H is normal ; :: thesis: contradiction
then consider a being Element of G such that
B2: H |^ a <> multMagma(# the carrier of H, the multF of H #) by GROUP_3:def 13;
consider f being inner Automorphism of G such that
B3: a is_inner_wrt f by Th32;
Image (f | H) = H |^ a by B3, Th28;
hence contradiction by B1, B2; :: thesis: verum