let O be set ; :: thesis: for G being strict GroupWithOperators of O holds G,G ./. ((1). G) are_isomorphic
let G be strict GroupWithOperators of O; :: thesis: G,G ./. ((1). G) are_isomorphic
nat_hom ((1). G) is bijective by Th54;
hence G,G ./. ((1). G) are_isomorphic ; :: thesis: verum