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