theorem Th54: :: GROUP_9:54

for O being set
for G being GroupWithOperators of O holds nat_hom ((1). G) is bijective