theorem Th56: :: GROUP_9:56

for O being set
for G being strict GroupWithOperators of O holds G,G ./. ((1). G) are_isomorphic