theorem Th17: :: GROUP_17:17

for H, K being finite Group holds card (product <*H,K*>) = (card H) * (card K)