let G be strict Group; :: thesis: for h being Homomorphism of G,G holds
( h in Aut G iff h is bijective )
let h be Homomorphism of G,G; :: thesis: ( h in Aut G iff h is bijective )

hereby :: thesis: ( h is bijective implies h in Aut G )

assume A1: h in Aut G ; :: thesis: h is bijective
then A2: h is onto by Def1;
h is one-to-one by A1, Def1;
then h is one-to-one ;
hence h is bijective by A2; :: thesis: verum

end;

thus ( h is bijective implies h in Aut G ) by Def1; :: thesis: verum