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 Th52;
then A1: nat_hom ((1). G) is one-to-one by Th66;
nat_hom ((1). G) is onto by Th69;
hence nat_hom ((1). G) is bijective by A1; :: thesis: verum