theorem Th2: :: GROUP_17:2

for H, K being non empty finite set holds card (product <*H,K*>) = (card H) * (card K)