theorem Th8: :: GROUP_22:8

for G being Group
for H, K being trivial Subgroup of G holds multMagma(# the carrier of H, the multF of H #) = multMagma(# the carrier of K, the multF of K #)