let G be Group; :: thesis: G,G ./. ((1). G) are_isomorphic
nat_hom ((1). G) is bijective by Th65;
hence G,G ./. ((1). G) are_isomorphic ; :: thesis: verum