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