theorem :: GROUP_9:67

for O being set
for G being strict Group ex H being strict GroupWithOperators of O st G = multMagma(# the carrier of H, the multF of H #)