theorem Th7: :: GROUP_22:7

for G being Group
for H being Subgroup of G st H is trivial holds
multMagma(# the carrier of H, the multF of H #) = (1). G