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