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