let G be Group; :: thesis: nat_hom ((1). G) is bijective
set g = nat_hom ((1). G);
Ker (nat_hom ((1). G)) = (1). G by Th43;
then nat_hom ((1). G) is one-to-one by Th56;
hence nat_hom ((1). G) is bijective by Th59; :: thesis: verum