let G be strict Group; :: thesis: for f being object holds
( f in Aut G iff f is Automorphism of G )
let f be object ; :: thesis: ( f in Aut G iff f is Automorphism of G )
thus ( f in Aut G implies f is Automorphism of G ) :: thesis: ( f is Automorphism of G implies f in Aut G )

proof

assume A1: f in Aut G ; :: thesis: f is Automorphism of G
then reconsider f = f as Endomorphism of G by AUTGROUP:def 1;
f is bijective by A1, AUTGROUP:def 1;
hence f is Automorphism of G ; :: thesis: verum

end;

thus ( f is Automorphism of G implies f in Aut G ) by AUTGROUP:def 1; :: thesis: verum